proposition: Lemma setC_bigcap J r (P : pred J) (F : J -> {set T}) : ~: (\bigcap_(j <- r | P j) F j) = \bigcup_(j <- r | P j) ~: F j.
proof: Proof. by apply: big_morph => [A B|]; rewrite ?setCT ?setCI. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)