n m : 0 < m -> m < n -> n - nat_pred m = (n - m).+1. Proof. revert m; snrapply gt_zero_ind. intros m H1. rewrite nat_sub_succ_r. rewrite nat_succ_pred. 1: reflexivity. apply equiv_lt_lt_sub. exact (lt_trans _ H1). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids