proposition: Lemma bounded_variationD a b f g : a < b -> BV a b f -> BV a b g -> BV a b (f \+ g).
proof: Proof. move=> ab [r abfr] [s abgs]; exists (r + s) => _ [l abl] <-. apply: le_trans; first exact: variation_le. rewrite lerD//. - by apply: abfr; exact: variations_variation. - by apply: abgs; exact: variations_variation. 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)