proposition: Lemma bigcup_max j U P F : P j -> U \subset F j -> U \subset \bigcup_(i | P i) F i.
proof: Proof. by move=> Pj sUF; apply: subset_trans (bigcup_sup _ Pj). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)