Major Section: ACL2-BUILT-INS
<= is a macro, and (<= x y) expands to the same thing as (not (< y x)). See <.
<=
(<= x y)
(not (< y x))
<= is a Common Lisp function. See any Common Lisp documentation for more information.