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

theorem WithBot.one_le_iff_pos {α : Type u_2} [PartialOrder α] [AddMonoidWithOne α] [ZeroLEOneClass α] [NeZero 1] [SuccAddOrder α] (a : WithBot α) : 1 ≤ a ↔ 0 < a