m n k : k <= m -> (n + m) - k = n + (m - k). Proof. intros H; induction n as [|n IHn] in |- *. - reflexivity. - change (?n.+1 + ?m) with (n + m).+1. lhs nrapply nat_sub_succ_l. 2: exact (ap nat_succ IHn). exact _. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids