proposition: Lemma int_fRN_lty : \int[mu]_x `|fRN x| < +oo.
proof: Proof. rewrite (@le_lt_trans _ _ M)//; last exact: sup_int_approxRN_lty. under eq_integral. by move=> x _; rewrite gee0_abs; last exact: fRN_ge0; over. rewrite int_fRN_lim// lime_le//; first exact: is_cvg_int_max_approxRN_seq. by apply: nearW => n; have [_ /andP[_ ]] := M_g_F n. 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