Adjoining top/bottom elements to ordered monoids.

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

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

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

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