rw [sum_pair hn]
case refine_2
n : ℕ
x : ℝ
hx : 0 ≤ x
hn : n ≠ 0
⊢ x ^ n / ↑n ! < Finset.sum {n, 0} fun i => x ^ i / ↑i !
case refine_2
n : ℕ
x : ℝ
hx : 0 ≤ x
hn : n ≠ 0
⊢ x ^ n / ↑n ! < x ^ n / ↑n ! + x ^ 0 / ↑0!