		Search-engine friendly clone of the ACL2 documentation.

Basic-products-with-negations

Rules for normalizing products with negative factors, and reciprocals of negations.

Theorem: functional-commutativity-of-minus-*-right

(defthm functional-commutativity-of-minus-*-right
  (equal (* x (- y)) (- (* x y))))

Theorem: functional-commutativity-of-minus-*-left

(defthm functional-commutativity-of-minus-*-left
  (equal (* (- x) y) (- (* x y))))

Theorem: reciprocal-minus

(defthm reciprocal-minus
  (equal (/ (- x)) (- (/ x))))