{n m} : n <= m <~> n - m = 0. Proof. srapply equiv_iff_hprop. - intro l; induction l. + exact (nat_sub_cancel n). + change (m.+1) with (1 + m). lhs nrapply nat_sub_r_add. lhs nrapply nat_sub_comm_r. by destruct IHl^. - induction n as [|n IHn] in m |- *. 1: intro; exact _. destruct m. + intros p; by destruct p. + intros p. apply leq_succ, IHn. exact p. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids