proposition: Lemma nondecreasing_total_variation a b f : a <= b -> {in `[a, b] &, nondecreasing_fun f} -> TV a b f = (f b - f a)%:E.
proof: Proof. rewrite le_eqVlt => /predU1P[<-{b} ?|ab ndf]. by rewrite total_variationxx subrr. rewrite /total_variation [X in ereal_sup X](_ : _ = [set (f b - f a)%:E]). by rewrite ereal_sup1. apply/seteqP; split => [x/= [s [t abt <-{s} <-{x}]]|x/= ->{x}]. by rewrite nondecreasing_variation. exists (variation a b f [:: b]) => //. exact/variations_variation/itv_partition1. by rewrite nondecreasing_variation//; exact: itv_partition1. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum finmap) mathcomp(matrix interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality) ereal reals signed topology prodnormedzmodule normedtype derive sequences real_interval HB(structures)