LT_CONV
reduceLib.LT_CONV : conv
Proves result of less-than ordering on two numerals.
If m and n are both numerals (e.g. 0, 1, 2, 3,...) of type
:num, then LT_CONV ``m < n`` returns the theorem:
|- (m < n) = T
if the natural number denoted by m is less than that denoted by n,
or
|- (m < n) = F
otherwise.
Failure
LT_CONV tm fails unless tm is of the form ``m < n``, where
m and n are numerals of natural number type (:num).
Example
> LT_CONV ``0 < 12``;
val it = |- 0 < 12 <=> T : thm
> LT_CONV ``13 < 13``;
val it = |- 13 < 13 <=> F : thm
> LT_CONV ``25 < 12``;
val it = |- 25 < 12 <=> F : thm