proposition: Lemma dompDl (D1 D2 : {freeg K}) : 0 <=g D1 -> 0 <=g D2 -> dom (D1 + D2) =i dom D1 ++ dom D2.
proof: Proof. move=> pos_D1 pos_D2 z; rewrite mem_cat !mem_dom coeffD. by rewrite paddr_eq0; first 1 [rewrite negb_and] || apply/fgposP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)