proposition: Lemma bigfcupsP (U : {fset T}) P F : reflect (forall i : I, i \in r -> P i -> F i `<=` U) (\bigcup_(i <- r | P i) F i `<=` U).
proof: Proof. apply: (iffP idP) => [sFU i ri Pi| sFU]. by apply: fsubset_trans sFU; apply: bigfcup_sup. by apply/fsubsetP=> x /bigfcupP[i /andP[ri Pi]]; apply/fsubsetP/sFU. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)