Documentation

Mathlib.Algebra.Order.SuccPred.WithBot

Algebraic properties of the successor function on WithBot #

source
theorem WithBot.succ_natCast {α : Type u_1} [Preorder α] [OrderBot α] [AddMonoidWithOne α] [SuccAddOrder α] (n : ℕ) :
(↑n).succ = ↑n + 1
source
@[simp]
theorem WithBot.succ_zero {α : Type u_1} [Preorder α] [OrderBot α] [AddMonoidWithOne α] [SuccAddOrder α] :
WithBot.succ 0 = 1
source
@[simp]
theorem WithBot.succ_one {α : Type u_1} [Preorder α] [OrderBot α] [AddMonoidWithOne α] [SuccAddOrder α] :
WithBot.succ 1 = 2
source
@[simp]
theorem WithBot.succ_ofNat {α : Type u_1} [Preorder α] [OrderBot α] [AddMonoidWithOne α] [SuccAddOrder α] (n : ℕ) [n.AtLeastTwo] :
(OfNat.ofNat n).succ = OfNat.ofNat n + 1