proposition: Lemma ereal_meets_gt (J : Type) (r : seq J) (P : {pred J}) (F : J -> \bar R) (u : \bar R) : u < +oo -> (forall x, P x -> u < F x) -> u < \meet_(x <- r | P x) F x.
proof: Proof. by move=>u0 ltFm; elim/big_rec: _ => // i x Px xu; rewrite ltxI ltFm. Qed.
imports: mathcomp(all_ssreflect ssrnum zmodp order constructive_ereal) preliminaries