proposition: Lemma domZ c D : c != 0 -> dom (c *: D) =i dom D.
proof: Proof. by move=> nz_c x; rewrite !mem_dom coeffZ mulf_eq0 negb_or nz_c. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)