rw [add_one]
A : Type ?u.204
inst✝³ : Inhabited A
inst✝² : Add A
inst✝¹ : Mul A
inst✝ : OfNat A 0
n : Nat
⊢ n < n + 1
A : Type ?u.204
inst✝³ : Inhabited A
inst✝² : Add A
inst✝¹ : Mul A
inst✝ : OfNat A 0
n : Nat
⊢ n < succ n