proposition: Lemma variation_itv_partitionLR a b c f s : a < c -> c < b -> itv_partition a b s -> variation a b f s <= variation a b f (itv_partitionL s c ++ itv_partitionR s c).
proof: Proof. move=> ac bc abs; have [cl|cl] := boolP (c \in s). by rewrite -in_itv_partition//; case: abs => /path_sorted. rewrite /itv_partitionL [in leLHS](notin_itv_partition _ cl)//; last first. by apply: path_sorted; case: abs => + _; exact. rewrite -notin_itv_partition//; last first. by apply: path_sorted; case: abs => /= + _; exact. rewrite !variation_zip//; last first. by apply: itv_partition_cat; [exact: (itv_partitionLP _ bc)|exact: (itv_partitionRP ac)]. rewrite [in leLHS](notin_itv_partition _ cl); last first. by apply: path_sorted; case: abs => + _; exact. set L := [seq x <- s | x < c]. rewrite -cats1 -catA. move: L => L. set B := itv_partitionR s c. move: B => B. elim/last_ind : L => [|L0 L1 _]. rewrite !cat0s /=; case: B => [|B0 B1]. by rewrite big_nil big_cons/= big_nil addr0. rewrite !big_cons/= addrA lerD// [leRHS]addrC. by rewrite (le_trans _ (ler_normD _ _))// addrA subrK. rewrite -cats1. rewrite (_ : a :: _ ++ B = (a :: L0) ++ [:: L1] ++ B)//; last first. by rewrite -!catA -cat_cons. rewrite zip_cat; last by rewrite cats1 size_rcons. rewrite (_ : a :: _ ++ _ ++ B = (a :: L0) ++ [:: L1] ++ [:: c] ++ B); last first. by rewrite -!catA -cat_cons. rewrite zip_cat; last by rewrite cats1 size_rcons. rewrite !big_cat lerD//. case: B => [|B0 B1]. by rewrite /= big_nil big_cons big_nil addr0. rewrite -cat1s zip_cat// catA. rewrite (_ : [:: L1] ++ _ ++ B1 = ([:: L1] ++ [:: c]) ++ [:: B0] ++ B1); last first. by rewrite catA. rewrite zip_cat// !big_cat lerD//= !big_cons !big_nil !addr0/= [leRHS]addrC. by rewrite (le_trans _ (ler_normD _ _))// addrA subrK. 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)