proposition: Lemma total_variation_ge a b f : a <= b -> (`|f b - f a|%:E <= TV a b f)%E.
proof: Proof. rewrite le_eqVlt => /predU1P[<-{b}|ab]. by rewrite total_variationxx subrr normr0. apply: ereal_sup_ub => /=; exists (variation a b f [:: b]). exact/variations_variation/itv_partition1. by rewrite /variation/= big_nat_recr//= big_nil add0r. 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)