proposition: Lemma domD_perm_eq D1 D2 : [predI (dom D1) & (dom D2)] =1 pred0 -> perm_eq (dom (D1 + D2)) (dom D1 ++ dom D2).
proof: Proof. move=> D12_nI; apply/uniq_perm; first exact: uniq_dom. rewrite cat_uniq !uniq_dom andbT; apply/hasPn => p p_in_D2. by move: (D12_nI p); rewrite /= p_in_D2 andbT => /negbT. move=> p; move: (D12_nI p); rewrite /= mem_cat !mem_dom coeffD. have [->|nz_D1p] /= := eqVneq (coeff p D1) 0; first by rewrite add0r. by move=> /negbFE /eqP ->; rewrite addr0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)