proposition: Lemma approximation : (forall t, D t -> (0 <= f t)%E) -> exists g : {nnsfun T >-> R}^nat, nondecreasing_seq (g : (T -> R)^nat) /\ (forall x, D x -> EFin \o g^~ x @ \oo --> f x).
proof: Proof. exists nnsfun_approx; split; [exact: nd_nnsfun_approx|]. by move=> x Dx; exact: cvg_nnsfun_approx. 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