proposition: Lemma Nat_induction1 (r:property): let s:= fun n => forall p, p <c n -> r p in (forall n, natp n -> s n -> r n) -> (forall n, natp n -> r n).
proof: Proof. move=> s si n nN; apply: (si)=>//. move: n nN; apply: Nat_induction; first by move=> p /clt0. move=> m mN sm p lp. case: (equal_or_not p m); first by move=>->; apply: si =>//. by move=> pm; apply: sm=>//; split=>//; apply /(cltSleP mN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)