proposition: Lemma meets_max_seq T (r : seq T) (P : {pred T}) (F : T -> L) (x : T) (u : L) : x \in r -> P x -> F x <= u -> \meet_(x <- r | P x) F x <= u.
proof: Proof. move=> ? ?; apply: le_trans; exact: meets_inf_seq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)