@@ -92,7 +92,12 @@ last {n=S _} = fS last
92total fSinjective : {f : Fin n} -> {f' : Fin n} -> (fS f = fS f') -> f = f'
92total fSinjective : {f : Fin n} -> {f' : Fin n} -> (fS f = fS f') -> f = f'
93fSinjective refl = refl
93fSinjective refl = refl
95−
95+instance Ord (Fin n) where
97+ compare fZ (fS _) = LT
98+ compare (fS _) fZ = GT
99+ compare (fS x) (fS y) = compare x y
96instance MinBound (Fin (S n)) where
101instance MinBound (Fin (S n)) where
97 minBound = fZ
102 minBound = fZ