proposition: Lemma Freeg_dom D : [freeg [seq (coeff x D, x) | x <- dom D]] = D.
proof: Proof. apply/esym/eqP/freeg_eqP=> k. rewrite -{1 2}[D]freeg_repr !coeff_Freeg /dom. case: (repr D)=> {}D rD /=; rewrite -map_comp map_id_in //. move=> [z x]; rewrite reduced_mem // => /andP [/eqP <- _]. by rewrite /= coeff_Freeg. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)