proposition: Lemma approxRN_seq_ex : { g : (T -> \bar R)^nat | forall k, g k \in approxRN /\ \int[mu]_x g k x > M - k.+1%:R^-1%:E }.
proof: Proof. pose P m g := g \in approxRN /\ M - m.+1%:R^-1%:E < \int[mu]_x g x. suff : { g : (T -> \bar R) ^nat & forall m, P m (g m)} by case => g ?; exists g. apply: (@choice _ _ P) => m. rewrite /P. have /(@ub_ereal_sup_adherent _ int_approxRN) : (0 < m.+1%:R^-1 :> R)%R. by rewrite invr_gt0. move/(_ sup_int_approxRN_fin_num) => [_ [h Gh <-]]. by exists h; rewrite inE; split => //; rewrite -/M in q. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets cardinality) mathcomp(functions fsbigop set_interval) HB(structures) reals ereal signed topology numfun normedtype sequences esum measure realfun lebesgue_measure lebesgue_integral