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