∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] {f : α → E}, eVariationOn (Function.rightLim f) Set.univ ≤ eVariationOn f Set.univ