proposition: Lemma variationsN a b f : variations a b (\- f) = variations a b f.
proof: Proof. apply/seteqP; split => [_ [s abs] <-|r [s abs]]. by rewrite variationN; exact: variations_variation. by rewrite -variationN => <-; 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)