[GOAL]
α : Type u_1
inst✝ : StrictOrderedSemiring α
n : ℕ
⊢ ↑n < ↑(n + 1)
[PROOFSTEP]
rw [Nat.cast_succ]
[GOAL]
α : Type u_1
inst✝ : StrictOrderedSemiring α
n : ℕ
⊢ ↑n < ↑n + 1
[PROOFSTEP]
apply lt_add_one
