proposition: Lemma bigcupsP U P F : reflect (forall i, P i -> F i \subset U) (\bigcup_(i | P i) F i \subset U).
proof: Proof. apply: (iffP idP) => [sFU i Pi| sFU]. by apply: subset_trans sFU; apply: bigcup_sup. by apply/subsetP=> x /bigcupP[i Pi]; apply: (subsetP (sFU i Pi)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)