proposition: Lemma Nat_induction4 (r:property) a b: natp a -> natp b -> r b -> (forall n, a <=c n -> n <c b -> r (csucc n) -> r n) -> (forall n, a <=c n -> n <=c b -> r n).
proof: Proof. move=> aN bN rb ti n an nb. set (q := fun n => ~ (r n)). case: (p_or_not_p (r n))=>// nrn. have nN:= NS_le_nat nb bN. have qi: (forall m, n <=c m -> m <c b -> q m -> q (csucc m)). rewrite /q;move=> m nm mb qm; dneg rs; apply: ti=> //; exact: cleT an nm. by move: ((Nat_induction3 nN bN nrn qi) _ nb (cleR (proj32 nb))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)