Don't need rfl after norm_num

Changes

1 changed files (+0/-1)

• Sum.lean
  • @@ -33,7 +33,6 @@ lemma telescope_sum (n : ℕ) (h : 2 ≤ n) :
    induction h with | refl => norm_num - rfl | step h ih => rw [sum_Ico_succ_top h, ih] simp