proposition: Lemma meetsP_seq T (r : seq T) (P : {pred T}) (F : T -> L) (l : L) : reflect (forall x : T, x \in r -> P x -> l <= F x) (l <= \meet_(x <- r | P x) F x).
proof: Proof. apply: (iffP idP) => leFm => [x xr Px|]. exact/(le_trans leFm)/meets_inf_seq. by rewrite big_seq_cond meets_ge// => x /andP[/leFm]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)