proposition: Lemma fgmap_f0_coeffE (D : {freeg K / G}) z : f 0 = 0 -> coeff z (fgmap D) = f (coeff z D) *+ P z.
proof: Proof. move=> z_f0; case zD: (z \in dom D). by rewrite fgmap_coeffE. rewrite !coeff_outdom ?z_f0 ?zD ?mul0rn //. by apply/negP=> /fgmap_dom; rewrite mem_filter zD andbF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)