∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) {s : Set α}
  {a b c : α},
  a ≤ b →
    b ≤ c →
      b ∈ s → eVariationOn f (s ∩ Set.Icc a b) + eVariationOn f (s ∩ Set.Icc b c) = eVariationOn f (s ∩ Set.Icc a c)