----------------------------------------------------------------------
GE_CONV                                                    (reduceLib)
----------------------------------------------------------------------
GE_CONV : conv

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

LIBRARY
reduce

DESCRIBE
If {m} and {n} are both numerals (e.g. {0}, {1}, {2}, {3},...), then
{GE_CONV "m >= n"} returns the theorem:

   |- (m >= n) = T

if the natural number denoted by {m} is greater than or equal to that
denoted by {n}, or

   |- (m >= n) = F

otherwise.

FAILURE
{GE_CONV tm} fails unless {tm} is of the form {"m >= n"}, where {m} and {n}
are numerals.

EXAMPLE

#GE_CONV "15 >= 14";;
|- 15 >= 14 = T

#GE_CONV "100 >= 100";;
|- 100 >= 100 = T

#GE_CONV "0 >= 107";;
|- 0 >= 107 = F


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