		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)))))))