α : Type u_1
β : Type ?u.8929
inst✝ : OrderedSemiring α
n : ℕ
⊢ ↑n ≤ ↑n + 1
α : Type u_1
β : Type ?u.8929
inst✝ : OrderedSemiring α
n : ℕ
⊢ ↑n ≤ ↑(n + 1)
rw [Nat.cast_succ]
no goals
α : Type u_1
β : Type ?u.8929
inst✝ : OrderedSemiring α
n : ℕ
⊢ ↑n ≤ ↑n + 1
exact le_add_of_nonneg_right zero_le_one