LESS_CONV : conv
STRUCTURE
wordsLib
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
HOL  Kananaskis-14