(in-package "ACL2")
(include-book "limits")
(in-theory (disable o< o+ o- o* o^))