proposition: Lemma bigfcup_sup j P F : j \in r -> P j -> F j `<=` \bigcup_(i <- r | P i) F i.
proof: Proof. move=> jr Pj; rewrite -bigfcup_undup big_mkcond. by rewrite (bigD1_seq j) ?mem_undup ?undup_uniq ?Pj //= fsubsetUl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)