proposition: Lemma increasing_prop1 p f: natp p -> (forall i, i <=c p -> natp (f i)) -> (forall n, n <c p -> (f n) <=c (f (csucc n))) -> (forall i j, i <=c j -> j <=c p -> (f i) <=c (f j)).
proof: Proof. move => pN p1 p2 i j lij ljp. move: (NS_le_nat ljp pN) => jN. move: j jN lij ljp. apply: Nat_induction; first by move => /cle0 -> /p1 /CS_nat /cleR. move => j jN Hrec /cle_eqVlt; case. by move => -> /p1 /CS_nat /cleR. move/(cltSleP jN) => lij ljp. exact: (cleT (Hrec lij (cleT (cleS jN) ljp)) (p2 _ (clt_leT (cltS jN) ljp))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)