proposition: Lemma variationD a b c f s t : a <= c -> c <= b -> itv_partition a c s -> itv_partition c b t -> variation a c f s + variation c b f t = variation a b f (s ++ t).
proof: Proof. rewrite le_eqVlt => /predU1P[<-{c} cb|ac]. by move=> /itv_partitionxx ->; rewrite variation_nil add0r. rewrite le_eqVlt => /predU1P[<-{b}|cb]. by move=> ? /itv_partitionxx ->; rewrite variation_nil addr0 cats0. move=> acs cbt; rewrite /variation /= [in RHS]/index_iota subn0 size_cat. rewrite iotaD add0n big_cat/= -[in X in _ = X + _](subn0 (size s)); congr +%R. rewrite -/(index_iota 0 (size s)) 2!big_nat. apply: eq_bigr => k /[!leq0n] /= ks. rewrite nth_cat ks -cat_cons nth_cat /= ltnS (ltnW ks). by rewrite !(set_nth_default b c)//= ltnS ltnW. rewrite -[in RHS](addnK (size s) (size t)). rewrite -/(index_iota (size s) (size t + size s)). rewrite -{1}[in RHS](add0n (size s)) big_addn addnK 2!big_nat; apply: eq_bigr. move=> k /[!leq0n]/= kt. rewrite nth_cat {1}(addnC k) -ltn_subRL subnn ltn0 addnK. case: k kt => [t0 /=|k kt]. rewrite add0n -cat_cons nth_cat/= ltnS leqnn -last_nth. by case: acs => _ /eqP ->. rewrite addSnnS (addnC k) -cat_cons nth_cat/= -ltn_subRL subnn ltn0. by rewrite -(addnC k) addnK. 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)