Lemma about subtraction in ordered monoids with a top element adjoined. #
instance
WithTop.instOrderedSubWithTopToLEPreorderToPreorderToPartialOrderToOrderedAddCommMonoidAddToAddToAddZeroClassToAddMonoidToAddCommMonoidInstSubWithTopToZero
{α : Type u_1}
[inst : CanonicallyOrderedAddMonoid α]
[inst : Sub α]
[inst : OrderedSub α]
:
OrderedSub (WithTop α)
Equations
- One or more equations did not get rendered due to their size.