proposition: Lemma expansion_prop8 f b k x (h:= Lg (csucc k) (fun i=> variant k x (Vg f i) i)) : expansion f b k -> natp x -> x <c b -> (expansion h b (csucc k) /\ expansion_value h b = (expansion_value f b) +c ((b ^c k) *c x)).
proof: Proof. move=> [bN kN b2 [fgf df vf]] xN xb. have eg: (expansion h b (csucc k)). hnf; rewrite /h; aw;split;fprops; split; fprops. move=> i idh; rewrite LgV//; move /(NleP kN): idh; case/cle_eqVlt. by move ->; rewrite variant_true0. move=> lik; rewrite (variant_false _ _ (proj2 lik)); apply: vf. by rewrite df; apply/NltP. have ck: cardinalp k by fprops. have ksk := (proj33 (cleS kN)). rewrite (expansion_prop7 eg ck); split; first by exact. have ->:(restr h k = f). rewrite /h; symmetry;apply: fgraph_exten; [ exact | fprops | aww | ]. rewrite df; move=> y ydf /=; rewrite !LgV//; fprops; rewrite variant_false //. by move/(NltP kN)/proj2: ydf. have -> //: (Vg h k *c (b ^c k) = (b ^c k) *c x). by rewrite cprodC /h LgV//;[ rewrite variant_true0 | apply: (Nsucc_i kN)]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)