num_CONV : conv
STRUCTURE
SYNOPSIS
Equates a non-zero numeral with the form SUC x for some x.
EXAMPLE
- num_CONV ``1203``;
> val it = |- 1203 = SUC 1202 : thm
FAILURE
Fails if the argument term is not a numeral of type ``:num``, or if the argument is ``0``.
SEEALSO
HOL  Kananaskis-14