@@ -95,9 +95,9 @@ instance MaxBound (Fin (S n)) where
96||| Substract two Fins, keeping the bound of the minuend
96||| Substract two Fins, keeping the bound of the minuend
97(-) : Fin n -> Fin m -> Fin n
97(-) : Fin n -> Fin m -> Fin n
98−(-) fZ _ = fZ
98+fZ - _ = fZ
99−(-) f fZ = f
99+f - fZ = f
100−(-) (fS f) (fS f') = weaken $ f - f'
100+(fS f) - (fS f') = weaken $ f - f'
102||| Multiply two Fins, extending the bound
102||| Multiply two Fins, extending the bound
103(*) : Fin n -> Fin m -> Fin (n * m)
103(*) : Fin n -> Fin m -> Fin (n * m)