proposition: Lemma expansion_prop7: (expansion_value g b) = (expansion_value (restr g k') b) +c (Vg g k' *c (b ^c k')).
proof: Proof. have k'n:= (expansion_prop4). pose h i := (Vg g i) *c (b ^c i). have ->: (Vg g k') *c (b ^c k') = h k' by []. move: (induction_on_sum h k'n). have <- : domain g = (csucc k') by move: Expg=> [_ _ _ [_ dg _]]. rewrite /expansion_value /restr Lgd => ->. by congr ( _ +c (h k')); apply:csumb_exten => x xi; rewrite LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)