@@ -93,6 +93,12 @@ instance MaxBound (Fin (S n)) where
93(+) {n=S n} {m=m} fZ f' = rewrite plusCommutative n m in weaken (weakenN n f')
93(+) {n=S n} {m=m} fZ f' = rewrite plusCommutative n m in weaken (weakenN n f')
94(+) (fS f) f' = fS (f + f')
94(+) (fS f) f' = fS (f + f')
96+||| Substract two Fins, keeping the bound of the minuend
97+(-) : Fin n -> Fin m -> Fin n
100+(-) (fS f) (fS f') = weaken $ f - f'
96||| Multiply two Fins, extending the bound
102||| Multiply two Fins, extending the bound
97(*) : Fin n -> Fin m -> Fin (n * m)
103(*) : Fin n -> Fin m -> Fin (n * m)
98(*) {n=Z} f f' = FinZElim f
104(*) {n=Z} f f' = FinZElim f