Adjoining top/bottom elements to ordered monoids.

instance WithTop.instIsOrderedAddMonoid {α : Type u} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] : IsOrderedAddMonoid (WithTop α)

instance WithBot.instIsOrderedAddMonoid {α : Type u} [AddCommMonoid α] [PartialOrder α] [IsOrderedAddMonoid α] : IsOrderedAddMonoid (WithBot α)

instance WithTop.canonicallyOrderedAdd {α : Type u} [Add α] [Preorder α] [CanonicallyOrderedAdd α] : CanonicallyOrderedAdd (WithTop α)

theorem WithBot.le_self_add {α : Type u} [Add α] [LE α] [CanonicallyOrderedAdd α] {x : WithBot α} (hx : x ≠ ⊥) (y : WithBot α) : y ≤ y + x

theorem WithBot.le_add_self {α : Type u} [AddCommMagma α] [LE α] [CanonicallyOrderedAdd α] {x : WithBot α} (hx : x ≠ ⊥) (y : WithBot α) : y ≤ x + y

@[simp]

theorem WithBot.top_add_of_ne_bot {α : Type u} [PartialOrder α] [OrderTop α] [Add α] [CanonicallyOrderedAdd α] {a : WithBot α} (h : a ≠ ⊥) : ⊤ + a = ⊤

@[simp]

theorem WithBot.add_top_of_ne_bot {α : Type u} [PartialOrder α] [OrderTop α] [Add α] [CanonicallyOrderedAdd α] {a : WithBot α} (h : a ≠ ⊥) : a + ⊤ = ⊤

theorem WithBot.lt_zero_iff_eq_bot {α : Type u_1} [AddMonoid α] [Preorder α] [CanonicallyOrderedAdd α] (a : WithBot α) : a < 0 ↔ a = ⊥