		Search-engine friendly clone of the ACL2 documentation.

Math-lemmas

Normalize-<-minus-/

Rewrite inequalities between 0 and negated or reciprocal terms, and (< (- x) (- y)).

Definitions and Theorems

Theorem: normalize-<-minus-/

(defthm normalize-<-minus-/
  (and (equal (< (- x) 0) (< 0 x))
       (equal (< 0 (- x)) (< x 0))
       (equal (< (- x) (- y)) (> x y))
       (implies (real/rationalp x)
                (and (equal (< 0 (/ x)) (< 0 x))
                     (equal (< (/ x) 0) (< x 0))))))