proposition: Lemma cumulative_content_sub_fsum (f : cumulative R) (D : {fset nat}) a0 b0 (a b : nat -> R) : (forall i, i \in D -> a i <= b i) -> `]a0, b0] `<=` \big[setU/set0]_(i <- D) `]a i, b i]%classic -> f b0 - f a0 <= \sum_(i <- D) (f (b i) - f (a i)).
proof: Proof. move=> Dab h; have [ab|ab] := leP a0 b0; last first. apply (@le_trans _ _ 0). by rewrite subr_le0 cumulative_is_nondecreasing// ltW. rewrite big_seq sumr_ge0// => i iD. by rewrite subr_ge0 cumulative_is_nondecreasing// Dab. have mab k : [set` D] k -> R.-ocitv.-measurable `]a k, b k]%classic by []. move: h; rewrite -bigcup_fset. move/(@content_sub_fsum _ R _ [the content _ _ of wlength f] _ [set` D] `]a0, b0]%classic (fun x => `](a x), (b x)]%classic) (finite_fset D) mab (is_ocitv _ _)) => /=. rewrite wlength_itv_bnd// -lee_fin => /le_trans; apply. rewrite -sumEFin fsbig_finite//= set_fsetK// big_seq [in X in (_ <= X)%E]big_seq. by apply: lee_sum => i iD; rewrite wlength_itv_bnd// Dab. 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