n m : m <= n -> n.+1 - m = (n - m).+1. Proof. intros H. induction m as [|m IHm] in n, H |- *. - by rewrite 2 nat_sub_zero_r. - simpl. rewrite nat_sub_succ_r. symmetry. apply nat_succ_pred. by apply equiv_lt_lt_sub. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids