rw [show n + 2 * m - (n + m) = m by omega]
n m : ℕ
f : ℕ → ℚ
⊢ ∑ k ∈ Finset.range (n + 2 * m - (n + m)), f (n + m + k) = ∑ x ∈ Finset.range m, f (n + (2 * m - 1 - x))
n m : ℕ
f : ℕ → ℚ
⊢ ∑ k ∈ Finset.range m, f (n + m + k) = ∑ x ∈ Finset.range m, f (n + (2 * m - 1 - x))