proposition: Lemma bigfcupP x F P : reflect (exists2 i : I, (i \in r) && P i & x \in F i) (x \in \bigcup_(i <- r | P i) F i).
proof: Proof. apply: (iffP idP) => [|[i /andP[ri Pi]]]; last first. by apply: fsubsetP x; rewrite bigfcup_sup. rewrite big_seq_cond; elim/big_rec: _ => [|i _ /andP[ri Pi] _ /fsetUP[|//]]. by rewrite in_fset0. by exists i; rewrite ?ri. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)