Data.Type.Natural.Class.Order

class PeanoOrder nat

data DiffNat n m

data LeqView n m

type family FlipOrdering (a :: Ordering) :: Ordering where ...

sFlipOrdering

coerceLeqL

coerceLeqR

sLeqCongL

sLeqCongR

sLeqCong

type n :-. m

(%:-.)

minPlusTruncMinus

truncMinusLeq