Separating the left-most term in a sum of Finset.range

Stream: new members

[spamegg]

import Mathlib
example (p : ℕ) : ∑ i ∈ Finset.range p, i = 0 + ∑ i ∈ Finset.Icc 1 (p-1), i := by
  sorry

[Ruben Van de Velde]

docs#Finset.sum_range_succ' is close

[Zhang Qinchuan]

If p=0,1 then your statement is correct by accident.

import Mathlib

example (p : ℕ) : ∑ i ∈ Finset.range p, i = 0 + ∑ i ∈ Finset.Icc 1 (p - 1), i := by
  match p with
  | 0 => norm_num
  | 1 => norm_num
  | p + 2 =>
    rw [show p + 2 = (p + 2 - 1) + 1 by omega, Finset.sum_range_succ', add_zero, zero_add]
    calc
      _ = ∑ i ∈ Finset.Ico 1 (p + 2), i := by
        rw [Finset.sum_Ico_eq_sum_range]
        apply Finset.sum_congr
        . congr
        . intros; rw [add_comm]
      _ = ∑ i ∈ Finset.Icc 1 (p + 1), i := by congr
      _ = _ := by congr