Proves what the truncated quotient of two natural number numerals is.
DESCRIPTION
If n and m are numerals (e.g. 0, 1, 2, 3,...), then
NUM_DIV_CONV `n DIV m` returns the theorem:
|- n DIV m = s
where s is the numeral that denotes the truncated quotient of the
numbers denoted by n and m.
FAILURE CONDITIONS
NUM_DIV_CONV tm fails if tm is not of the form `n DIV m`, where n and
m are numerals, or if the second numeral m is zero.
EXAMPLE
# NUM_DIV_CONV `99 DIV 9`;;
val it : thm = |- 99 DIV 9 = 11
# NUM_DIV_CONV `334 DIV 3`;;
val it : thm = |- 334 DIV 3 = 111
# NUM_DIV_CONV `11 DIV 0`;;
Exception: Failure "NUM_DIV_CONV".
COMMENTS
For definiteness, quotients with zero denominator are in fact designed to be
zero. However, it is perhaps bad style to rely on this fact, so the conversion
just fails in this case.