nat_ind_strong@{u} (P : nat -> Type@{u}) (IH_strong : forall n, (forall m, m < n -> P m) -> P n) : forall n, P n. Proof. intros n. apply IH_strong. simple_induction n n IHn; intros m H. 1: contradiction (not_lt_zero_r m). apply leq_pred' in H. apply equiv_leq_lt_or_eq in H. destruct H as [H|p]. - by apply IHn. - destruct p. by apply IH_strong. Defined.
Require Import Basics.Overture Basics.Tactics Basics.PathGroupoids