proposition: Lemma variation_rev_opp a b f s : itv_partition (- b) (- a) s -> variation a b f (rev (belast b (map -%R s))) = variation (- b) (- a) (f \o -%R) s.
proof: Proof. move=> abs; rewrite [in RHS]variation_opp_rev ?opprK//. suff: (f \o -%R) \o -%R = f by move=> ->. by apply/funext=> ? /=; rewrite opprK. 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)