proposition: Lemma variations_opp a b f : variations (- b) (- a) (f \o -%R) = variations a b f.
proof: Proof. rewrite eqEsubset; split=> [_ [s bas <-]| _ [s abs <-]]. eexists; last exact: variation_rev_opp. by move/itv_partition_rev : bas; rewrite !opprK. eexists; last by exact/esym/variation_opp_rev. exact: itv_partition_rev abs. 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)