O>=

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

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