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