@@ -98,6 +98,12 @@ instance MaxBound (Fin (S n)) where
9898(+) {n=S n} {m=m} fZ f' = rewrite plusCommutative n m in weaken (weakenN n f')
9999(+) (fS f) f' = fS (f + f')
100100
101+||| Substract two Fins, keeping the bound of the minuend
102+(-) : Fin n -> Fin m -> Fin n
103+fZ - _ = fZ
104+f - fZ = f
105+(fS f) - (fS f') = weaken $ f - f'
106+
101107||| Multiply two Fins, extending the bound
102108(*) : Fin n -> Fin m -> Fin (n * m)
103109(*) {n=Z} f f' = FinZElim f