proposition: Lemma variation_next a b f s : itv_partition a b s -> variation a b f s = \sum_(x <- belast a s) `|f (next (locked (a :: s)) x) - f x|.
proof: Proof. move=> [] sa /eqP asb; rewrite /variation [in LHS]/= (big_nth b) !big_nat. rewrite size_belast; apply: eq_bigr => i /andP[_ si]. congr (`| f _ - f _ |); last first. by rewrite lastI -cats1 nth_cat size_belast// si. rewrite -lock next_nth. rewrite {1}lastI mem_rcons inE mem_nth ?size_belast// orbT. rewrite lastI -cats1 index_cat mem_nth ?size_belast//. rewrite index_uniq ?size_belast//. exact: set_nth_default. have /lt_sorted_uniq : sorted <%R (a :: s) by []. by rewrite lastI rcons_uniq => /andP[]. 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)