@@ -98,6 +98,12 @@ instance MaxBound (Fin (S n)) where
98(+) {n=S n} {m=m} fZ f' = rewrite plusCommutative n m in weaken (weakenN n f')
98(+) {n=S n} {m=m} fZ f' = rewrite plusCommutative n m in weaken (weakenN n f')
99(+) (fS f) f' = fS (f + f')
99(+) (fS f) f' = fS (f + f')
101+||| Substract two Fins, keeping the bound of the minuend
102+(-) : Fin n -> Fin m -> Fin n
105+(fS f) - (fS f') = weaken $ f - f'
101||| Multiply two Fins, extending the bound
107||| Multiply two Fins, extending the bound
102(*) : Fin n -> Fin m -> Fin (n * m)
108(*) : Fin n -> Fin m -> Fin (n * m)
103(*) {n=Z} f f' = FinZElim f
109(*) {n=Z} f f' = FinZElim f