proposition: Lemma bounded_variationl a c b f : a <= c -> c <= b -> BV a b f -> BV a c f.
proof: Proof. rewrite le_eqVlt => /predU1P[<-{c} ? ?|ac]; first exact: bounded_variationxx. rewrite le_eqVlt => /predU1P[<-{b}//|cb]. move=> [x Hx]; exists x => _ [s acs] <-. rewrite (@le_trans _ _ (variation a b f (rcons s b)))//; last first. apply/Hx/variations_variation; case: acs => sa /eqP asc. by rewrite /itv_partition rcons_path last_rcons sa/= asc. rewrite {2}/variation size_rcons -[leLHS]addr0 big_nat_recr//= lerD//. rewrite /variation !big_nat ler_sum// => k; rewrite leq0n /= => ks. rewrite nth_rcons// ks -cats1 -cat_cons nth_cat /= ltnS (ltnW ks). by rewrite ![in leRHS](set_nth_default c)//= ltnS ltnW. 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)