proposition: Lemma bigcap_setU A B F : (\bigcap_(i in A :|: B) F i) = (\bigcap_(i in A) F i) :&: (\bigcap_(i in B) F i).
proof: Proof. by apply: setC_inj; rewrite setCI !setC_bigcap bigcup_setU. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)