proposition: Lemma variation_prev a b f s : itv_partition a b s -> variation a b f s = \sum_(x <- s) `|f x - f (prev (locked (a :: s)) x)|.
proof: Proof. move=> [] sa /eqP asb; rewrite /variation [in LHS]/= (big_nth b) !big_nat. apply: eq_bigr => i /andP[_ si]; congr (`| _ - f _ |). rewrite -lock. rewrite prev_nth inE gt_eqF; last first. rewrite -[a]/(nth b (a :: s) 0) -[ltRHS]/(nth b (a :: s) i.+1). exact: lt_sorted_ltn_nth. rewrite orFb mem_nth// index_uniq//. by apply: set_nth_default => /=; rewrite ltnS ltnW. by apply: (sorted_uniq lt_trans) => //; apply: path_sorted sa. 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)