proposition: Lemma variation_zip a b f s : itv_partition a b s -> variation a b f s = \sum_(x <- zip s (a :: s)) `|f x.1 - f x.2|.
proof: Proof. elim: s a b => // [a b|h t ih a b]. by rewrite /itv_partition /= => -[_ /eqP <-]; rewrite /variation/= !big_nil. rewrite /itv_partition /variation => -[]/= /andP[ah ht] /eqP htb. rewrite big_nat_recl//= big_cons/=; congr +%R. have /ih : itv_partition h b t by split => //; exact/eqP. by rewrite /variation => ->; rewrite !big_seq; apply/eq_bigr => r rt. 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)