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