NUM_LT_CONV : conv
|- n < m <=> T or |- n < m <=> F
# NUM_LT_CONV `42 < 42`;; val it : thm = |- 42 < 42 <=> F # NUM_LT_CONV `11 < 19`;; val it : thm = |- 11 < 19 <=> T