proposition: Lemma fgmap_coeffE (D : {freeg K / G}) z : z \in dom D -> coeff z (fgmap D) = f (coeff z D) *+ P z.
proof: Proof. move=> zD; rewrite /fgmap raddf_sum /= -big_filter; case Pz: (P z). + rewrite (bigD1_seq z) ?(filter_uniq, uniq_dom) //=; last first. by rewrite mem_filter Pz. rewrite coeffU eqxx mulr1 big1 ?addr0 //. by move=> z' ne_z'z; rewrite coeffU (negbTE ne_z'z) mulr0. + rewrite big_seq big1 ?mulr0 //. move=> z' z'PD; rewrite coeffU; have/negbTE->: z' != z. apply/eqP=> /(congr1 (fun x => x \in filter P (dom D))). by rewrite z'PD mem_filter Pz. by rewrite mulr0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)