proposition: Lemma nondecreasing_right_continuousP (R : numFieldType) (a : R) (e : R) (f : cumulative R) : e > 0 -> exists d : {posnum R}, f (a + d%:num) <= f a + e.
proof: Proof. move=> e0; move: (cumulative_is_right_continuous f). move=> /(_ a)/(@cvgr_dist_lt _ [the normedModType R of R^o]). move=> /(_ _ e0)[] _ /posnumP[d] => h. exists (PosNum [gt0 of (d%:num / 2)]) => //=. move: h => /(_ (a + d%:num / 2)) /=. rewrite opprD addrA subrr distrC subr0 ger0_norm //. rewrite ltr_pdivrMr// ltr_pMr// ltr1n => /(_ erefl). rewrite ltrDl divr_gt0// => /(_ erefl). rewrite ler0_norm; last first. by rewrite subr_le0 (cumulative_is_nondecreasing f)// lerDl. by rewrite opprB ltrBlDl => fa; exact: ltW. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) HB(structures) mathcomp.classical(mathcomp_extra boolp classical_sets) mathcomp.classical(functions fsbigop cardinality) reals ereal signed topology numfun normedtype sequences esum real_interval measure realfun