• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • Arithmetic
    • Bit-vectors
      • Sparseint
      • Bitops
      • Bv
      • Ihs
        • Logops-definitions
        • Math-lemmas
          • Prefer-*-to-/
          • ACL2-numberp-algebra
          • Integerp-+-minus-*
          • Rewrite-linear-equalities-to-iff
          • Ihs-math
          • Rationalp-algebra
          • Normalize-<-/-to-*-3
          • Expt-algebra
          • Cancel-equal-+-*
          • Normalize-<-/-to-*
          • Normalize-<-minus-/
          • Normalize-equal-/-to-*
          • Normalize-equal-0
          • Integerp-algebra
        • Ihs-theories
        • Ihs-init
        • Logops
      • Rtl
    • Algebra
  • Testing-utilities

• Math-lemmas
• Prefer-*-to-/

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