----------------------------------------------------------------------
LESS_CONV                                                   (wordsLib)
----------------------------------------------------------------------
LESS_CONV : conv

SYNOPSIS
Converts terms of the form {n < m} into
{(n = m - 1) \/ ... \/ (n = 1) \/ (n = 0)}, provided that {m} is a natural
number literal.

EXAMPLE

> wordsLib.LESS_CONV ``n < 4n``;
val it =
   |- n < 4 <=> (n = 3) \/ (n = 2) \/ (n = 1) \/ (n = 0):
   thm


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