have hnk : n + m ≤ n + 2 * m := by omega
n m : ℕ
f : ℕ → ℚ
hmn : n ≤ n + m
⊢ ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i
n m : ℕ
f : ℕ → ℚ
hmn : n ≤ n + m
hnk : n + m ≤ n + 2 * m
⊢ ∑ i ∈ Finset.Ico n (n + 2 * m), f i = ∑ i ∈ Finset.Ico n (n + m), f i + ∑ i ∈ Finset.Ico (n + m) (n + 2 * m), f i