Untitled

example (n : Nat): ∑ k in range (n+1), (k ^ (2 : ℕ) : ℕ) = (n*(n+1)*(2*n+1)) / 6 := by
  symm
  apply Nat.div_eq_of_eq_mul_left (by norm_num)
  symm
  induction n with
  | zero =>
    simp
  | succ n ih =>
    rw[sum_range_succ]
    rw[right_distrib]
    rw[ih]
    rw[succ_eq_add_one]
    ring