proposition: Lemma expansion_prop9 f b k: expansion f b k -> (expansion_value f b) <c (b ^c k).
proof: Proof. move=> Exp. have kN: natp k by move: Exp => [bN kN _ _]. move: k kN f Exp. apply: Nat_induction. move: clt_01 => H g [bN _ b2 [fgf df _]]. rewrite cpowx0 /expansion_value df/csumb csum_trivial; aw; trivial. move=> n nN pn g eg. have cn: (cardinalp n) by fprops. rewrite (expansion_prop7 eg cn). have er:= (expansion_prop5 eg cn). have [bN _ b2 [fgf df vg]] := eg. move: (pn _ er). rewrite cpow_succ //. move: (expansion_prop3 er). set (a0:= expansion_value (restr g n) b). set (b0:= b ^c n); set c0:= (Vg g n) *c b0. move => a0N h. have p1: (Vg g n) <c b by apply: vg; rewrite df; apply:Nsucc_i. have cN:= NS_lt_nat p1 bN. have b0N: natp b0 by apply: NS_pow. have le1: (a0 +c c0) <c (b0 +c c0). apply: csum_Mlteq => //;rewrite /c0; fprops. suff le2: (b0 +c c0) <=c (b0 *c b) by apply: clt_leT le1 le2. have cb: cardinalp b0 by fprops. have ->: b0 +c c0 = b0 *c (csucc (Vg g n)). rewrite (Nsucc_rw cN) cprodDr (cprod1r cb) cprodC csumC //. by apply: cprod_Meqle;apply /(cleSltP cN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)