proposition: Lemma divisibiliy_by_nine f k: expansion_ten f k -> let g:= (Lg (domain f) (fun i=> (Vg f i) *c (\10c ^c i))) in (csum g) = (csum f) %c[mod \9c].
proof: Proof. move=> [p1 p2 p3 p4]. have ep: expansion f \10c k. split => //; [by apply: NS10 | apply:cgt10_1]. exact (eqmod_pow3 NS9 card9_nz ep card_mod_10_9). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)