Extra utilities for working with Nats
Subtraction gives a result that is actually smaller.
If n + 1 < m, then n < m
Convert from LT' to LTE
If n < m, then 1 + n < 1 + m
Division and modulus on Nat
, inspired by the definition in the
Agda standard library.
This uses well-founded recursion on LT'
.
the dividend
the divisor
division by zero is nonsense
Zero is less than any non-zero number.
A strict less-than relation on Nat
.
the smaller number
the larger number
The result of division on natural numbers.
the dividend
the divisor
The result of division, with a quotient and a remainder.
the dividend
the divisor
the quotient
the remainder (bounded by the divisor)
the fact that this is, in fact, a result of division