proposition: Lemma increasing_nat_prop p n: natp p -> natp n -> forall f, (inc f (functions_incr_nat p n) <-> inc f (functions p n) /\ forall i j, i <=c j -> j <c p -> Vf f i <=c Vf f j).
proof: Proof. move => pN nN f. move:(proj2 (Nintco_wor p)) (proj2 (Nintco_wor n)). rewrite (NintE pN)(NintE nN)=> sr1 sr2. split. move => /Zo_P []; rewrite sr1 sr2 => ha hb; split => // i j lij lin. have la: gle (Nint_co p) i j. by apply /(Nintco_gleP pN). by move: hb => [_ _ _ fp]; move: (fp i j la) =>/(Nintco_gleP nN)/proj1 . move =>[qa qb]; apply/Zo_P; rewrite sr1 sr2; split => //. split => //. - exact:(proj1 (proj1(Nintco_wor p))). - exact:(proj1 (proj1(Nintco_wor n))). - by rewrite sr1 sr2; apply/functionsP. - move => i j /(Nintco_gleP pN) [lij ljp]. move:(qb _ _ lij ljp) => le1. apply/(Nintco_gleP nN); split => //; apply /(NltP nN). by move/functionsP: qa =>[ff sf <-]; Wtac; rewrite sf; apply /(NltP pN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)