proposition: Lemma domD_subset D1 D2 : {subset dom (D1 + D2) <= dom D1 ++ dom D2}.
proof: Proof. move=> z; rewrite mem_cat !mem_dom coeffD. have nz_sum (x1 x2 : R): x1 + x2 != 0 -> (x1 != 0) || (x2 != 0). by have [->|] := eqVneq x1 0; first by rewrite add0r. by move=> /nz_sum /orP [] ->; rewrite ?orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)