@@ -93,6 +93,12 @@ instance MaxBound (Fin (S n)) where
9393(+) {n=S n} {m=m} fZ f' = rewrite plusCommutative n m in weaken (weakenN n f')
9494(+) (fS f) f' = fS (f + f')
9595
96+||| Substract two Fins, keeping the bound of the minuend
97+(-) : Fin n -> Fin m -> Fin n
98+(-) fZ _ = fZ
99+(-) f fZ = f
100+(-) (fS f) (fS f') = weaken $ f - f'
101+
96102||| Multiply two Fins, extending the bound
97103(*) : Fin n -> Fin m -> Fin (n * m)
98104(*) {n=Z} f f' = FinZElim f