proposition: Lemma meetsP I (l : L) (P : {pred I}) (F : I -> L) : reflect (forall i : I, P i -> l <= F i) (l <= \meet_(i | P i) F i).
proof: Proof. by apply: (iffP (meetsP_seq _ _ _ _)) => H ? ?; apply: H. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)