proposition: Lemma dom_sum_subset (I : Type) (r : seq I) (F : I -> {freeg K / R}) (P : pred I) : {subset dom (\sum_(i <- r | P i) F i) <= flatten [seq dom (F i) | i <- r & P i]}.
proof: Proof. move=> p; elim: r => [|r rs IH]; first by rewrite big_nil dom0. rewrite big_cons; case Pr: (P r); last by move/IH=> /=; rewrite Pr. move/domD_subset; rewrite mem_cat /= Pr => /orP[|/IH]. + by rewrite map_cons /= mem_cat=> ->. + by rewrite map_cons /= mem_cat=> ->; rewrite orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)