proposition: Lemma bounded_variationr a c b f : a <= c -> c <= b -> BV a b f -> BV c b f.
proof: Proof. rewrite le_eqVlt => /predU1P[<-{c}//|ac]. rewrite le_eqVlt => /predU1P[<-{b} ?|cb]; first exact: bounded_variationxx. move=> [x Hx]; exists x => _ [s cbs] <-. rewrite (@le_trans _ _ (variation a b f (c :: s)))//; last first. apply/Hx/variations_variation; case: cbs => cs csb. by rewrite /itv_partition/= ac/= cs. by rewrite {2}/variation/= -[leLHS]add0r big_nat_recl//= lerD. 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)