NUM_GT_CONV : conv
|- n > m <=> T or |- n > m <=> F
# NUM_GT_CONV `3 > 2`;; val it : thm = |- 3 > 2 <=> T # NUM_GT_CONV `77 > 77`;; val it : thm = |- 77 > 77 <=> F