nat_double_ind_leq@{u} (P : nat -> nat -> Type@{u}) (Hn0 : forall n, P n 0) (Hnn : forall n, P n n) (IH : forall n m, m < n -> (forall m', m' <= n -> P n m') -> P n.+1 m.+1) : forall n m, m <= n -> P n m. Proof. intro n; simple_induction n n IHn; intros m H. - destruct (path_zero_leq_zero_r m H)^; clear H. apply Hn0. - destruct m. + apply Hn0. + apply equiv_leq_lt_or_eq in H. destruct H as [H | []]. 2: apply Hnn. rapply IH. rapply IHn. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids