proposition: Lemma expansion_prop2: finite_int_fam (Lg (domain f) (fun i=> (Vg f i) *c (b ^c i))).
proof: Proof. have [bN kN b2 [fgf df vf]] := Exp. hnf; rewrite /allf; aw; split. move=> i idf; rewrite LgV//; move /expansion_prop0P: idf => idf. apply: (NS_prod (expansion_prop1 idf) (NS_pow bN (NS_lt_nat idf kN))). by rewrite df; apply: finite_set_nat. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)