proposition: Lemma expansion_prop10 f b k: cardinalp k -> expansion f b (csucc k) -> cdivision_prop (expansion_value f b) (b ^c k) (Vg f k) (expansion_value (restr f k) b).
proof: Proof. move=> ck ie;split. by rewrite csumC cprodC; apply: expansion_prop7. by apply: expansion_prop9; apply: expansion_prop5. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)