n m k (p : n <= k) (q : n <= m) (r : m.+1 = k) : p = r # leq_succ_r q. Proof. revert m q r. destruct p. + intros k p r. destruct r. contradiction (lt_irrefl _ p). + intros m' q r. pose (r' := path_nat_succ _ _ r). destruct r'. assert (t : idpath = r) by apply path_ishprop. destruct t. cbn. apply ap. destruct q. 1: apply leq_refl_inj. apply ( n m _ p q idpath). Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids