Algebraic properties of the successor function on WithBot

theorem WithBot.succ_natCast {α : Type u_1} [Preorder α] [OrderBot α] [AddMonoidWithOne α] [SuccAddOrder α] (n : ℕ) : (↑n).succ = ↑n + 1

@[simp]

theorem WithBot.succ_zero {α : Type u_1} [Preorder α] [OrderBot α] [AddMonoidWithOne α] [SuccAddOrder α] : succ 0 = 1

@[simp]

theorem WithBot.succ_one {α : Type u_1} [Preorder α] [OrderBot α] [AddMonoidWithOne α] [SuccAddOrder α] : succ 1 = 2

@[simp]

theorem WithBot.succ_ofNat {α : Type u_1} [Preorder α] [OrderBot α] [AddMonoidWithOne α] [SuccAddOrder α] (n : ℕ) [n.AtLeastTwo] : (OfNat.ofNat n).succ = OfNat.ofNat n + 1