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