@@ -20,6 +20,9 @@ class Preorder t (po : t -> t -> Type) where
2020class (Preorder t po) => Poset t (po : t -> t -> Type) where
2121 total antisymmetric : (a : t) -> (b : t) -> po a b -> po b a -> a = b
2222
23+class (Poset t to) => Ordered t (to : t -> t -> Type) where
24+ total order : (a : t) -> (b : t) -> Either (to a b) (to b a)
25+
2326--------------------------------------------------------------------------------
2427-- Natural numbers
2528--------------------------------------------------------------------------------
@@ -56,6 +59,10 @@ total zeroNeverGreater : {n : Nat} -> NatLTE (S n) Z -> _|_
5659zeroNeverGreater {n} (nLTESm _) impossible
5760zeroNeverGreater {n} nEqn impossible
5861
62+total zeroAlwaysSmaller : {n : Nat} -> NatLTE Z n
63+zeroAlwaysSmaller {n = Z } = nEqn
64+zeroAlwaysSmaller {n = S k} = nLTESm (zeroAlwaysSmaller {n = k})
65+
5966total
6067nGTSm : {n : Nat} -> {m : Nat} -> (NatLTE n m -> _|_) -> NatLTE n (S m) -> _|_
6168nGTSm disprf (nLTESm nLTEm) = FalseElim (disprf nLTEm)
@@ -74,5 +81,23 @@ decideNatLTE x (S y) with (decEq x (S y))
7481instance Decidable [Nat,Nat] NatLTE where
7582 decide = decideNatLTE
7683
84+total
7785lte : (m : Nat) -> (n : Nat) -> Dec (NatLTE m n)
7886lte m n = decide {ts = [Nat,Nat]} {p = NatLTE} m n
87+
88+total
89+shift : (m : Nat) -> (n : Nat) -> NatLTE m n -> NatLTE (S m) (S n)
90+shift Z Z _ = nEqn
91+shift Z (S Z) _ = nLTESm nEqn
92+shift Z (S (S j)) _ = nLTESm (shift Z (S j) zeroAlwaysSmaller)
93+shift (S k) Z prf = FalseElim (zeroNeverGreater prf)
94+shift (S k) (S k) nEqn = nEqn
95+shift (S k) (S j) (nLTESm prf) = nLTESm (shift (S k) j prf)
96+
97+instance Ordered Nat NatLTE where
98+ order Z n = Left zeroAlwaysSmaller
99+ order m Z = Right zeroAlwaysSmaller
100+ order (S k) (S j) with (order k j)
101+ order (S k) (S j) | Left prf = Left (shift k j prf)
102+ order (S k) (S j) | Right prf = Right (shift j k prf)
103+