proposition: Lemma expansion_prop11 f g b k: cardinalp k -> expansion f b (csucc k) -> expansion g b (csucc k) -> (Vg f k) <c (Vg g k) -> (expansion_value f b) <c (expansion_value g b).
proof: Proof. move=> ck ef eg ltk. rewrite (expansion_prop7 ef ck) (expansion_prop7 eg ck). have ef1:= (expansion_prop5 ef ck). have eg1:=(expansion_prop5 eg ck). move: (expansion_prop9 ef1). move: (expansion_prop3 ef1). move: (expansion_prop3 eg1). set u:= expansion_value _ _; set v:= expansion_value _ _. move=> uN vN vp. have kn:= (expansion_prop4 ef ck). have fN:=(expansion_prop6 ef ck). have gN:=(expansion_prop6 eg ck). set (B:= b ^c k). have bN: natp b by move: ef => [h _]. have BN: natp B by rewrite /B; fprops. apply: (@clt_leT (B +c ((Vg f k) *c B))). apply: csum_Mlteq; fprops. apply: (@cleT ((Vg g k) *c B)); last by apply:csum_Mle0; fprops. move /(cleSltP fN): ltk => ltk. move: (cprod_Mleeq B ltk). by rewrite (Nsucc_rw fN) cprodDl (cprod1l (CS_nat BN)) csumC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)