Rules about rfix.
Theorem: rfix-when-rationalp
(defthm rfix-when-rationalp (implies (rationalp x) (equal (rfix x) x)))
Theorem: rationalp-of-rfix
(defthm rationalp-of-rfix (rationalp (rfix x)))
