proposition: Lemma mem_dom D x : (x \in dom D) = (coeff x D != 0).
proof: Proof. elim/quotW: D; case=> D rD. rewrite /dom (perm_mem (perm_map _ (perm_eq_fgrepr _))) /=. unlock coeff; rewrite !piE /lift /= -precoeffE. case/andP: rD => uniqD /allP /= rD; rewrite precoeff_uniqE //. apply/idP/idP; last apply: contra_neqT; move=> x_in_D; last first. by rewrite nth_default // memNindex // !size_map. rewrite (nth_map (0, x)); last first. by rewrite -(size_map (@snd _ _)) index_mem x_in_D. by apply/rD/mem_nth; rewrite -(size_map (@snd _ _)) index_mem. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)