LESS_CONV

wordsLib.LESS_CONV : conv

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