proposition: Lemma expansion_prop13 f g b kf kg l: kf <=c l -> l <c kg -> expansion f b kf -> expansion g b kg -> Vg g l <> \0c -> (expansion_value f b) <c (expansion_value g b).
proof: Proof. move=> le1 le2 ef eg vnz. apply: (@clt_leT (b ^c kf)); first apply: (expansion_prop9 ef). move: eg => [bN bK b2 [fgf df vg]]. rewrite /expansion_value /csumb. set F:= Lg _ _. have fgF: fgraph F by rewrite /F;fprops. have dF: domain F = kg by rewrite /F -df; aw. have alc: (forall x, inc x (domain F) -> cardinalp (Vg F x)). rewrite dF -df /F => x xdf; rewrite LgV //; fprops. have ldf: inc l (domain F) by rewrite dF; apply /NltP. set j:= singleton l. have sj: sub j (domain F) by move => t /set1_P ->. move: (csum_increasing1 sj). rewrite (csum_trivial4 _ _ ) (card_card (alc _ ldf)). have ldg: inc l (domain g) by rewrite df; apply /NltP. have bnz: b<> \0c by move=>h; rewrite h in b2; case: (clt0 b2). apply:cleT; rewrite /F LgV//. apply: (@cleT (b ^c l)); first apply: cpow_Mlele; fprops. rewrite cprodC;apply: cprod_M1le; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)