{n m} : (n <= m) <~> (n < m) + (n = m). Proof. srapply equiv_iff_hprop. - nrapply ishprop_sum. 1,2: exact _. intros H1 p; destruct p. contradiction (lt_irrefl _ _). - intro l; induction l. + by right. + left; exact (leq_succ l). - intros [l|p]. + exact (leq_succ_l l). + destruct p. exact (leq_refl _). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids