{n m} : n <= m -> m - (m - n) = n. Proof. intros H; induction H. - by rewrite nat_sub_cancel, nat_sub_zero_r. - rewrite (nat_sub_succ_l m n); only 2: exact _. exact IHleq. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids