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