proposition: Lemma divisibiliy_by_three 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 \3c].
proof: Proof. move=> [p1 p2 p3 p4]. have ep: expansion f \10c k. split => //; [by apply: NS10 | apply:cgt10_1]. exact (eqmod_pow3 NS3 card3_nz ep card_mod_10_3). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)