n m : n - m.+1 = nat_pred (n - m). Proof. induction n as [|n IHn] in m |- *. 1: reflexivity. destruct m. 1: apply nat_sub_zero_r. apply IHn. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids