Major Section: ACL2-BUILT-INS
O>= is a macro and (o>= x y) expands to (not (o< x y)). See o<.
O>=
(o>= x y)
(not (o< x y))