proposition: Lemma strict_increasing_prop2: (forall i j, i <=c j -> j <c p -> ((f i) -c i) <=c ((f j) -c j)).
proof: Proof. case: (equal_or_not p \0c). move => -> i j ij jp; case: (clt0 jp). move=> pnz. have [qN ps] := (cpred_pr pN pnz). set q := cpred p. have fq: finite_c (cpred p) by fprops. pose g i := (f i) -c i. have q1: (forall i : Set, i <=c q -> natp (g i)). by move=> i ip; apply: NS_diff; apply: fN; rewrite ps;apply/(cltSleP qN). have q2:forall n, n <c q -> (g n) <=c (g (csucc n)). move=> n np. have nN:= (NS_lt_nat np qN). have hy:=(strict_increasing_prop1). have p1: (csucc n) <c p by rewrite ps; apply: cltSS. have p2:= (cle_ltT (cleS nN) p1). move: (hy _ p1) (hy _ p2)=> qp1 qp2. move: (fN p1)(fN p2) => s1 s2. apply/(cltSleP (NS_diff(csucc n) s1)); rewrite - (csucc_diff s1 nN qp1). apply: (cdiff_pr7 qp2 (fm (cltS nN) p1) s1). move=> i j ij jp. apply: (increasing_prop1 qN q1 q2 ij). by move: jp; rewrite {1} ps; move /(cltSleP qN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)