LE_CONV

reduceLib.LE_CONV : conv

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

If m and n are both numerals (e.g. 0, 1, 2, 3,…), then LE_CONV "m <= n" returns the theorem:

   |- (m <= n) = T

if the natural number denoted by m is less than or equal to that denoted by n, or

   |- (m <= n) = F

otherwise.

Failure

LE_CONV tm fails unless tm is of the form "m <= n", where m and n are numerals.

Example

#LE_CONV "12 <= 198";;
|- 12 <= 198 = T

#LE_CONV "46 <= 46";;
|- 46 <= 46 = T

#LE_CONV "13 <= 12";;
|- 13 <= 12 = F