proposition: Lemma eqmod_pow3 f b k: expansion f b k -> b = \1c %c[mod B] -> expansion_value f b = csum f %c[mod B].
proof: Proof. move=> ep b1. have kN: natp k by move: ep => [bN kN _]. move: k kN f ep. apply: Nat_induction. move=> g [bN _ b2 [fgf df _]]. by rewrite /expansion_value/csumb df !csum_trivial //; aw. move=> n nN pn g eg. have cn: (cardinalp n) by fprops. rewrite (expansion_prop7 eg cn). move: (expansion_prop5 eg cn) => er. move: (eg) => [bN _ _ [fgg dg _]]. move: (NS_succ nN) => snN. have si: sub n (domain g) by rewrite dg; apply (proj33 (cleS nN)). have ->: (csum g = (csum (restr g n)) +c (Vg g n)). pose h w := \0c +c (Vg g w). have hp: forall x, inc x (domain g) -> h x = Vg g x. move=> x; rewrite dg; move /(NltP snN) => p1. move: (expansion_prop1 eg p1) => p2. by rewrite /h Nsum0l. move: (induction_on_sum h nN); rewrite /csumb. have ->: h n = Vg g n by apply: hp; rewrite dg; apply:Nsucc_i. have ->: (Lg (csucc n) h = g). apply: fgraph_exten; fprops; first by aw. aw; move=> x xd /=; rewrite LgV //; apply: hp; ue. have -> //: (Lg n h = (restr g n)). apply: Lg_exten => x xb; apply: (hp _ (si _ xb)). have p1: natp (Vg g n) by apply: (expansion_prop1 eg (cltS nN)). have p2: natp ((Vg g n) *c (b ^c n)). apply: (NS_prod p1 (NS_pow bN nN)). have p3: natp (csum (restr g n)). apply: finite_sum_finite_aux; last by exact. split => //. move=> i; rewrite dg; move /(NltP snN). apply: (expansion_prop1 eg). by rewrite dg; apply: finite_set_nat. apply: (eqmod_sum (expansion_prop3 er) p2 p3 p1 (pn _ er)). apply: (eqmod_pow2 bN p1 nN b1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)