proposition: Lemma bigcup_set0P (P : set U) (F : U -> set T) : reflect (exists i, P i /\ F i !=set0) (\bigcup_(i in P) F i != set0).
proof: Proof. apply: (iffP idP). - by case/set0P => a [] i Si Fia; exists i; split; [ | exists a]. - by case=> i [] Si [] a Fia; apply/set0P; exists a, i. Qed.
imports: mathcomp(all_ssreflect) mathcomp(boolp classical_sets)