NUM_GE_CONV : conv

SYNOPSIS

Proves whether one numeral is greater than or equal to another.

DESCRIPTION

If n and m are two numerals (e.g. 0, 1, 2, 3,...), then NUM_GE_CONV `n >= m` returns:

   |- n >= m <=> T       or       |- n >= m <=> F

depending on whether the natural number represented by n is greater than or equal to the one represented by m.

FAILURE CONDITIONS

NUM_GE_CONV tm fails if tm is not of the form `n >= m`, where n and m are numerals.

EXAMPLE

  # NUM_GE_CONV `1 >= 0`;;
  val it : thm = |- 1 >= 0 <=> T

  # NUM_GE_CONV `181 >= 211`;;
  val it : thm = |- 181 >= 211 <=> F

USES

Performing basic arithmetic reasoning while producing a proof.

SEE ALSO