proposition: Lemma nonincreasing_variation a b f s : {in `[a, b] &, nonincreasing_fun f} -> itv_partition a b s -> variation a b f s = f a - f b.
proof: Proof. move=> /nonincreasing_funN ndNf abs; have := nondecreasing_variation ndNf abs. by rewrite opprK addrC => <-; rewrite variationN. 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)