NUM_MOD_CONV : term -> thm

SYNOPSIS
Proves what the remainder on dividing one natural number numeral by another is.

DESCRIPTION
If n and m are numerals (e.g. 0, 1, 2, 3,...), then NUM_MOD_CONV `n MOD m` returns the theorem:
   |- n MOD m = s
where s is the numeral that denotes the remainder on dividing the number denoted by n by the one denoted by m.

FAILURE CONDITIONS
NUM_MOD_CONV tm fails if tm is not of the form `n MOD m`, where n and m are numerals, or if the second numeral m is zero.

EXAMPLE
  # NUM_MOD_CONV `1089 MOD 9`;;
  val it : thm = |- 1089 MOD 9 = 0

  # NUM_MOD_CONV `1234 MOD 3`;;
  val it : thm = |- 1234 MOD 3 = 1

  # NUM_MOD_CONV `11 MOD 0`;;
  Exception: Failure "NUM_MOD_CONV".

COMMENTS
For definiteness, remainders 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_DIV_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_MULT_CONV, NUM_ODD_CONV, NUM_PRE_CONV, NUM_REDUCE_CONV, NUM_RED_CONV, NUM_REL_CONV, NUM_SUB_CONV, NUM_SUC_CONV.