proposition: Lemma fgmap_dom D : {subset dom (fgmap D) <= filter P (dom D)}.
proof: Proof. move=> z; rewrite mem_dom mem_filter andbC. case zD: (z \in (dom D)) => /=. + rewrite fgmap_coeffE //; case: (P _)=> //=. by rewrite mulr0n eqxx. + rewrite /fgmap raddf_sum /= big_seq_cond big1 ?eqxx //. move=> z' /andP [z'D _]; rewrite coeffU. have/negbTE->: z' != z; last by rewrite mulr0. apply/eqP=> /(congr1 (fun x => x \in dom D)). by rewrite zD z'D. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)