LT_CONV : conv
STRUCTURE
reduceLib
SYNOPSIS
Proves result of less-than ordering on two numerals.
LIBRARY
reduce
DESCRIPTION
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
GT_CONV
HOL  Kananaskis-13