		Search-engine friendly clone of the ACL2 documentation.

Normalize-<-/-to-*-3

Rewrite: Replace x < y/z and x > y/z with x*z < y or x*z > y, depending on the sign of z.

Definitions and Theorems

Theorem: normalize-<-/-to-*-3

(defthm normalize-<-/-to-*-3
        (implies (and (real/rationalp x)
                      (real/rationalp y)
                      (real/rationalp z)
                      (not (equal z 0)))
                 (and (equal (< x (* y (/ z)))
                             (if (< z 0)
                                 (< y (* x z))
                                 (< (* x z) y)))
                      (equal (< x (* (/ z) y))
                             (if (< z 0)
                                 (< y (* x z))
                                 (< (* x z) y)))
                      (equal (< (* y (/ z)) x)
                             (if (< z 0)
                                 (< (* x z) y)
                                 (< y (* x z))))
                      (equal (< (* (/ z) y) x)
                             (if (< z 0)
                                 (< (* x z) y)
                                 (< y (* x z)))))))