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