proposition: Lemma variation_subseq a b f (s t : list R) : itv_partition a b s -> itv_partition a b t -> subseq s t -> variation a b f s <= variation a b f t.
proof: Proof. elim: t s a => [? ? ? /= _ /eqP ->//|a s IH [|x t] w]. by rewrite variation_nil // variation_ge0. move=> /[dup] /itv_partition_cons itvxb /[dup] /itv_partition_le wb itvxt. move=> /[dup] /itv_partition_cons itvas itvws /=. have ab : a <= b by exact: (itv_partition_le itvas). have wa : w < a by case: itvws => /= /andP[]. have waW : w <= a := ltW wa. case: ifPn => [|] nXA. move/eqP : nXA itvxt itvxb => -> itvat itvt /= ta. rewrite -[_ :: t]cat1s -[_ :: s]cat1s. rewrite -?(@variationD _ _ a)//; [|exact: itv_partition1..]. by rewrite lerD// IH. move=> xts; rewrite -[_ :: s]cat1s -(@variationD _ _ a) => //; last first. exact: itv_partition1. have [y [s' s'E]] : exists y s', s = y :: s'. by case: {itvas itvws IH} s xts => // y s' ?; exists y, s'. apply: (@le_trans _ _ (variation w b f s)). rewrite IH//. case: itvws => /= /andP[_]; rewrite s'E /= => /andP[ay ys' lyb]. by split => //; rewrite (path_lt_head wa)//= ys' andbT. by rewrite variationD //; [exact: le_variation | exact: itv_partition1]. 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)