proposition: Lemma true_below_rec (P:property) n: natp n -> (forall i, i <c (csucc n) -> P i) -> (forall i, i<c n -> P i) /\ P n.
proof: Proof. move => nN H; split. move => k kn; apply: H; exact:(clt_leT kn (cleS nN)). by apply: H; apply: cltS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)