NUM_DIV_CONV : term -> thm

SYNOPSIS
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.

SEE ALSO
NUM_ADD_CONV, NUM_EQ_CONV, NUM_EVEN_CONV, NUM_EXP_CONV, NUM_FACT_CONV, NUM_GE_CONV, NUM_GT_CONV, NUM_LE_CONV, NUM_LT_CONV, NUM_MAX_CONV, NUM_MIN_CONV, NUM_MOD_CONV, NUM_MULT_CONV, NUM_ODD_CONV, NUM_PRE_CONV, NUM_REDUCE_CONV, NUM_RED_CONV, NUM_REL_CONV, NUM_SUB_CONV, NUM_SUC_CONV.