		Search-engine friendly clone of the ACL2 documentation.

Normalize-equal-/-to-*

Rewrite: Replace x = y/z with x*z = y.

Definitions and Theorems

Theorem: normalize-equal-/-to-*

(defthm normalize-equal-/-to-*
  (implies (and (acl2-numberp z) (not (equal z 0)))
           (and (equal (equal x (* y (/ z)))
                       (and (acl2-numberp x)
                            (equal (* x z) (fix y))))
                (equal (equal x (* (/ z) y))
                       (and (acl2-numberp x)
                            (equal (* x z) (fix y)))))))