O<=

the less-than-or-equal relation for the ordinals 
Major Section:  ACL2-BUILT-INS

o<= is a macro and (o<= x y) expands to (not (o< y x)). See o<.