module Control.EqOrd

--Eq and Ord compatibility
public export
interface Ord ty => EqOrd ty where
    eqord : (x, y : ty) -> (x == y) = (compare x y == EQ)

export
EqOrd Nat where
    eqord 0 0 = Refl
    eqord 0 (S _) = Refl
    eqord (S _) 0 = Refl
    eqord (S i) (S j) = eqord i j