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,...), 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.
EXAMPLE
#LT_CONV "0 < 12";;
|- 0 < 12 = T

#LT_CONV "13 < 13";;
|- 13 < 13 = F

#LT_CONV "25 < 12";;
|- 25 < 12 = F
HOL  Kananaskis-8