proposition: Lemma Nat_induction3 (r:property) a b: natp a -> natp b -> r a -> (forall n, a <=c n -> n <c b -> r n -> r (csucc n)) -> (forall n, a <=c n -> n <=c b -> r n).
proof: Proof. move=> aN bN ra ri n an nb. have nN:= NS_le_nat nb bN. move: n nN an nb; apply: Nat_induction. by move => az _; rewrite -(cle0 az). move=> m mN sm am; move/(cleSltP mN) => mb. case: (equal_or_not a (csucc m));[ by move => <- | move=> asm]. move/(cltSleP mN): (conj am asm) => leam. apply: (ri _ leam mb (sm leam (proj1 mb))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)