O>

the greater-than relation for the ordinals 
Major Section:  ACL2-BUILT-INS

O> is a macro and (o> x y) expands to (o< y x). See o<.