proposition: Lemma le_approx k x (f0 : forall x, D x -> (0 <= f x)%E) : D x -> ((approx k x)%:E <= f x)%E.
proof: Proof. move=> Dx; have [fixoo|] := ltP (f x) (+oo%E); last first. by rewrite leye_eq => /eqP ->; rewrite leey. have nd_ag : {homo approx ^~ x : n m / (n <= m)%N >-> n <= m}. by move=> m n mn; exact/lefP/nd_approx. have fi0 y : D y -> (0 <= f y)%E by move=> ?; exact: f0. have cvg_af := cvg_approx fi0 Dx fixoo. have is_cvg_af : cvgn (approx ^~ x) by apply/cvg_ex; eexists; exact: cvg_af. have {is_cvg_af} := nondecreasing_cvgn_le nd_ag is_cvg_af k. rewrite -lee_fin => /le_trans; apply. rewrite -(@fineK _ (f x)); last by rewrite ge0_fin_numE// f0. by move/(cvg_lim (@Rhausdorff R)) : cvg_af => ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure numfun