proposition: Lemma finI_fromI {I : choiceType} T D (f : I -> set T) A B : finI_from D f A -> finI_from D f B -> finI_from D f (A `&` B) .
proof: Proof. case=> N ND <- [M MD <-]; exists (N `|` M)%fset. by move=> ?; rewrite inE => /orP[/ND | /MD]. by rewrite -bigcap_setU set_fsetU. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed