other
(in-package "ACL2")
include-book
(include-book "arithmetic-3/bind-free/top" :dir :system)
include-book
(include-book "arithmetic-3/floor-mod/floor-mod" :dir :system)
include-book
(include-book "ext")
other
(add-default-hints! '((nonlinearp-default-hint stable-under-simplificationp hist pspv)))
in-theory
(in-theory (enable strong-expt-type-prescription-rules))