proposition: Lemma int_fRNE : \int[mu]_x fRN x = M.
proof: Proof. apply/eqP; rewrite eq_le; apply/andP; split. rewrite int_fRN_lim// lime_le//; first exact: is_cvg_int_max_approxRN_seq. by apply: nearW => n; have [_ /andP[_]] := M_g_F n. rewrite int_fRN_lim//. have cvgM : (M - m.+1%:R^-1%:E) @[m --> \oo] --> M. rewrite -[X in _ --> X]sube0; apply: cvgeB. + by rewrite fin_num_adde_defl. + exact: cvg_cst. + apply/fine_cvgP; split; first exact: nearW. rewrite [X in X @ _ --> _](_ : _ = (fun x => x.+1%:R^-1))//. apply/gtr0_cvgV0; first exact: nearW. apply/cvgrnyP. rewrite [X in X @ _](_ : _ = fun n => n + 1)%N; first exact: cvg_addnr. by apply/funext => n; rewrite addn1. apply: (@le_trans _ _ (lim (M - m.+1%:R^-1%:E @[m --> \oo]))). by move/cvg_lim : cvgM => ->. apply: lee_lim; [by apply/cvg_ex; exists M|exact: is_cvg_int_max_approxRN_seq|]. apply: nearW => m. by have [/[swap] /andP[? _] /ltW/le_trans] := M_g_F m; exact. 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