Documentation

Counterexamples.OrderedCancelAddCommMonoidWithBounds

Do not combine OrderedCancelAddCommMonoid with BoundedOrder #

This file shows that combining OrderedCancelAddCommMonoid with BoundedOrder is not a good idea, as such a structure must be trivial (⊥ = x = ⊤ for all x). The same applies to any superclasses, e.g. combining StrictOrderedSemiring with CompleteLattice.