Provides definitional axiom for a nonzero numeral.
DESCRIPTION
num_CONV is an axiom-scheme from which one may obtain a defining equation for
any numeral not equal to 0 (i.e. 1, 2, 3,...). If
`n` is such a constant, then num_CONV `n` returns the theorem:
|- n = SUC m
where m is the numeral that denotes the predecessor of the
number denoted by n.
FAILURE CONDITIONS
num_CONV tm fails if tm is `0` or if not tm is not a numeral.