proposition: Lemma strict_increasing_prop3 n: natp n -> (forall i, i <c p -> (f i) <c (n +c p)) -> (forall i, i <c p -> ((f i) -c i) <=c n).
proof: Proof. move=> nN fb i ip. case: (equal_or_not p \0c) => h. rewrite h in ip;case: (clt0 ip). have [qN psq] := (cpred_pr pN h). move:ip; rewrite psq; move /(cltSleP qN)=> iq. have qp: ((cpred p) <c p) by rewrite {2} psq; aww. apply: (@cleT ((f (cpred p)) -c (cpred p))). exact: (strict_increasing_prop2 iq qp). have aa:= (strict_increasing_prop1 qp). have csp :=(cdiff_pr aa). move: (fb _ qp); rewrite - {1} csp. have sN: natp ((cpred p) +c n) by fprops. rewrite {4} psq (csum_nS _ qN) (csumC n) => /(cltSleP sN). by move/(csum_le2l qN (NS_diff (cpred p) (fN qp)) nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)