product

(in-package "ACL2")

(local (include-book "product-proofs"))

(defthm product-less-than-zero
  (implies (case-split (or (not (complex-rationalp x)) (not (complex-rationalp y))))
    (equal (< (* x y) 0)
      (if (< x 0)
        (< 0 y)
        (if (equal 0 x)
          nil
          (if (not (acl2-numberp x))
            nil
            (< y 0)))))))

(defthm product-greater-than-zero
  (implies (case-split (not (complex-rationalp y)))
    (equal (< 0 (* x y))
      (or (and (< 0 x) (< 0 y)) (and (< y 0) (< x 0))))))

(defthm product-greater-than-zero-2
  (implies (case-split (not (complex-rationalp x)))
    (equal (< 0 (* x y))
      (or (and (< 0 x) (< 0 y)) (and (< y 0) (< x 0))))))

(defthm product-equal-zero
  (equal (equal 0 (* x y))
    (if (not (acl2-numberp x))
      t
      (if (not (acl2-numberp y))
        t
        (if (equal 0 x)
          t
          (equal 0 y))))))