n m (p : n <= m.+1) (q : n <= m) : p = leq_succ_r q := leq_succ_r_inj_gen n m m.+1 p q idpath. Global Instance ishprop_leq n m : IsHProp (n <= m). Proof. apply hprop_allpath. intros p q; revert p. induction q. + intros y. rapply leq_refl_inj. + intros y. rapply . Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids