∀ {α : Type u_2} {E : Type u_1} [inst : PseudoEMetricSpace E] (f : α → E) (n : ℕ) (u v : ℕ → α),
  ∑ i ∈ Finset.range n, edist (f (u (i + 1))) (f (u i)) =
    ∑ i ∈ Finset.range n,
      edist (f (if i + 1 ≤ n then u (i + 1) else v (i + 1 - (n + 1)))) (f (if i ≤ n then u i else v (i - (n + 1))))