1\DOC
2
3\TYPE {LESS_CONV : conv}
4
5\SYNOPSIS
6
7Converts terms of the form {n < m} into
8{(n = m - 1) \/ ... \/ (n = 1) \/ (n = 0)}, provided that {m} is a natural
9number literal.
10
11\EXAMPLE
12{
13> wordsLib.LESS_CONV ``n < 4n``;
14val it =
15   |- n < 4 <=> (n = 3) \/ (n = 2) \/ (n = 1) \/ (n = 0):
16   thm
17}
18
19\ENDDOC
20