NUM_LE_CONV : conv
|- n <= m <=> T or |- n <= m <=> F
# NUM_LE_CONV `12 <= 19`;; val it : thm = |- 12 <= 19 <=> T # NUM_LE_CONV `12345 <= 12344`;; val it : thm = |- 12345 <= 12344 <=> F