# Lemma about subtraction in ordered monoids with a top element adjoined. #

This file introduces a subtraction on `WithTop α`

when `α`

has a subtraction and a bottom element,
given by `x - ⊤ = ⊥`

and `⊤ - x = ⊤`

. This will be instantiated mostly for `ℕ∞`

and `ℝ≥0∞`

, where
the bottom element is zero.

Note that there is another subtraction on objects of the form `WithTop α`

in the file
`Mathlib.Algebra.Order.Group.WithTop`

, setting `-⊤ = ⊤`

as this corresponds to the additivization
of the usual convention `0⁻¹ = 0`

and is relevant in valuation theory. Since this other instance
is only registered for `LinearOrderedAddCommGroup α`

(which doesn't have a bottom element, unless
the group is trivial), this shouldn't create diamonds.

If `α`

has a subtraction and a bottom element, we can extend the subtraction to `WithTop α`

, by
setting `x - ⊤ = ⊥`

and `⊤ - x = ⊤`

.

## Instances For

## Equations

- ⋯ = ⋯