----------------------------------------------------------------------
GT_CONV                                                    (reduceLib)
----------------------------------------------------------------------
GT_CONV : conv

SYNOPSIS
Proves result of greater-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 {GT_CONV "m > n"} returns the theorem:

   |- (m > n) = T

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

   |- (m > n) = F

otherwise.

FAILURE
{GT_CONV tm} fails unless {tm} is of the form {``m > n``}, where {m} and {n}
are numerals of type {:num}.

EXAMPLE

> GT_CONV ``100 > 10``;
val it = |- 100 > 10 <=> T : thm

> GT_CONV ``15 > 15``;
val it = |- 15 > 15 <=> F : thm

> GT_CONV ``11 > 27``;
val it = |- 11 > 27 = F : thm


SEEALSO
reduceLib.LT_CONV.

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