proposition: Lemma strict_increasing_prop1: (forall i, i <c p -> i <=c (f i)).
proof: Proof. move=> i lip. have iN:= NS_lt_nat lip pN. move: i iN lip; apply: Nat_induction. by move=> /fN /CS_nat h;apply: cle0x. move=> n nN pn aux. have le2:=(cltS nN). have le3:=(fm le2 aux). have le4:= (pn (clt_ltT le2 aux)). apply /cleSlt0P; [ fprops | fprops | exact:cle_ltT le4 le3]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)