proposition: Lemma bigcup0P P F : reflect (forall i, P i -> F i = set0) (\bigcup_(i | P i) F i == set0).
proof: Proof. rewrite -subset0; apply: (iffP bigcupsP) => sub0 i /sub0; last by move->. by rewrite subset0 => /eqP. Qed.
imports: mathcomp(all_ssreflect)