proposition: Lemma bigcup_disjointP U P F : reflect (forall i : I, P i -> [disjoint U & F i]) [disjoint U & \bigcup_(i | P i) F i].
proof: Proof. apply: (iffP idP) => [dUF i Pp|dUF]. by apply: disjointWr dUF; apply: bigcup_sup. rewrite disjoint_sym disjoint_subset. by apply/bigcupsP=> i /dUF; rewrite disjoint_sym disjoint_subset. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)