rw [Finset.sum_add_distrib, add_right_inj]
n m : ℕ
f : ℕ → ℚ
⊢ ∑ x ∈ Finset.range m, f (n + x) + ∑ k ∈ Finset.range (n + 2 * m - (n + m)), f (n + m + k) =
    ∑ i ∈ Finset.range m, (f (n + i) + f (n + (2 * m - 1 - i)))
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))