		Search-engine friendly clone of the ACL2 documentation.

Normalize-<-/-to-*

Rewrite: Replace x < 1/y with x*y < 1 or x*y > 1, based on the sign of y.

Definitions and Theorems

Theorem: normalize-<-/-to-*

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