----------------------------------------------------------------------
LT_CONV                                                    (reduceLib)
----------------------------------------------------------------------
LT_CONV : conv

SYNOPSIS
Proves result of less-than ordering on two numerals.

LIBRARY
reduce

DESCRIBE
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


SEEALSO
reduceLib.GT_CONV.

----------------------------------------------------------------------