num_CONV
numLib.num_CONV : conv
Equates a non-zero numeral with the form SUC x for some x.
Example
> numLib.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``.