(in-package "ACL2")
(include-book "xdoc/constructors" :dir :system)
(defsection std/basic/nfix :parents (std/basic nfix) :short "Rules about @(tsee nfix)." (defthm nfix-when-natp (implies (natp x) (equal (nfix x) x))) (defthmd natp-of-nfix (natp (nfix x))))