simple-equalities-and-inequalities

Included Books

building-blocks top simplify-helper simple-equalities-and-inequalities-helper

other

(in-package "ACL2")

include-book

(include-book "building-blocks")

local

(local (include-book "../../support/top"))

local

(local (include-book "simplify-helper"))

local

(local (include-book "simple-equalities-and-inequalities-helper"))

other

(set-state-ok t)

|(equal (- x) c)|theorem

(defthm |(equal (- x) c)|
  (implies (and (syntaxp (numeric-constant-p c))
      (syntaxp (mostly-negative-addends-p x mfc state))
      (acl2-numberp c)
      (acl2-numberp x))
    (equal (equal x c) (equal (- x) (- c)))))

|(equal c (- x))|theorem

(defthm |(equal c (- x))|
  (implies (and (syntaxp (numeric-constant-p c))
      (syntaxp (mostly-negative-addends-p x mfc state))
      (acl2-numberp c)
      (acl2-numberp x))
    (equal (equal c x) (equal (- x) (- c)))))

|(equal (/ x) c)|theorem

(defthm |(equal (/ x) c)|
  (implies (and (syntaxp (numeric-constant-p c))
      (syntaxp (mostly-divisive-factors-p x mfc state))
      (syntaxp (simplify-ok-p `(equal ,X ,C)
          '(equal (unary-/ x) (unary-/ c))
          `((x . ,X) (c . ,C))
          mfc
          state))
      (acl2-numberp c)
      (acl2-numberp x))
    (equal (equal x c) (equal (/ x) (/ c)))))

|(equal c (/ x))|theorem

(defthm |(equal c (/ x))|
  (implies (and (syntaxp (numeric-constant-p c))
      (syntaxp (mostly-divisive-factors-p x mfc state))
      (syntaxp (simplify-ok-p `(equal ,X ,C)
          '(equal (unary-/ x) (unary-/ c))
          `((x . ,X) (c . ,C))
          mfc
          state))
      (acl2-numberp c)
      (acl2-numberp x))
    (equal (equal c x) (equal (/ x) (/ c)))))

|(equal (- x) (- y))|theorem

(defthm |(equal (- x) (- y))|
  (implies (and (syntaxp (mostly-negative-addends-p x mfc state))
      (syntaxp (mostly-negative-addends-p y mfc state))
      (acl2-numberp x)
      (acl2-numberp y))
    (equal (equal x y) (equal (- x) (- y)))))

|(equal (/ x) (/ y))|theorem

(defthm |(equal (/ x) (/ y))|
  (implies (and (syntaxp (mostly-divisive-factors-p x mfc state))
      (syntaxp (mostly-divisive-factors-p y mfc state))
      (syntaxp (simplify-ok-p `(equal ,X ,Y)
          '(equal (unary-/ x) (unary-/ y))
          `((x . ,X) (y . ,Y))
          mfc
          state))
      (acl2-numberp x)
      (acl2-numberp y))
    (equal (equal x y) (equal (/ x) (/ y)))))

local

(local (in-theory (disable floor)))

integerp-<-constanttheorem

(defthm integerp-<-constant
  (implies (and (syntaxp (rational-constant-p c))
      (real/rationalp c)
      (not (integerp c))
      (integerp x))
    (equal (< x c) (<= x (floor c 1))))
  :otf-flg t)

constant-<-integerptheorem

(defthm constant-<-integerp
  (implies (and (syntaxp (rational-constant-p c))
      (real/rationalp c)
      (not (integerp c))
      (integerp x))
    (equal (< c x) (<= (+ 1 (floor c 1)) x)))
  :otf-flg t)

|(< (- x) c)|theorem

(defthm |(< (- x) c)|
  (implies (and (syntaxp (numeric-constant-p c))
      (syntaxp (mostly-negative-addends-p x mfc state)))
    (equal (< x c) (< (- c) (- x)))))

|(< c (- x))|theorem

(defthm |(< c (- x))|
  (implies (and (syntaxp (numeric-constant-p c))
      (syntaxp (mostly-negative-addends-p x mfc state)))
    (equal (< c x) (< (- x) (- c)))))

|(< (/ x) 0)|theorem

(defthm |(< (/ x) 0)|
  (implies (and (syntaxp (mostly-divisive-factors-p x mfc state))
      (syntaxp (simplify-ok-p `(< ,X '0)
          '(< (unary-/ x) '0)
          `((x . ,X))
          mfc
          state))
      (real/rationalp x))
    (equal (< x 0) (< (/ x) 0))))

|(< 0 (/ x))|theorem

(defthm |(< 0 (/ x))|
  (implies (and (syntaxp (mostly-divisive-factors-p x mfc state))
      (syntaxp (simplify-ok-p `(< '0 ,X)
          '(< '0 (unary-/ x))
          `((x . ,X))
          mfc
          state))
      (real/rationalp x))
    (equal (< 0 x) (< 0 (/ x)))))

local

(local (in-theory (enable prefer-*-to-/)))

|(< (/ x) c) negative c --- present in goal|theorem

(defthm |(< (/ x) c) negative c --- present in goal|
  (implies (and (syntaxp (numeric-constant-p c))
      (real/rationalp c)
      (< c 0)
      (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (let ((parity (present-in-goal `(< ,X ,C) mfc state)))
          (cond ((eq parity 'positive) t)
            ((eq parity 'negative) (not (proveably-integer 'x `((x . ,X)) mfc state)))
            (t nil))))
      (syntaxp (mostly-divisive-factors-p x mfc state))
      (real/rationalp x))
    (equal (< x c) (and (< (/ x) 0) (< (/ c) (/ x))))))

|(< (/ x) c) negative c --- obj t or nil|theorem

(defthm |(< (/ x) c) negative c --- obj t or nil|
  (implies (and (syntaxp (numeric-constant-p c))
      (real/rationalp c)
      (< c 0)
      (syntaxp (let ((obj (mfc-obj x mfc state)))
          (or (eq obj 't)
            (and (eq obj 'nil)
              (not (proveably-integer 'x `((x . ,X)) mfc state))))))
      (syntaxp (mostly-divisive-factors-p x mfc state))
      (real/rationalp x))
    (equal (< x c) (and (< (/ x) 0) (< (/ c) (/ x))))))

|(< (/ x) c) positive c --- present in goal|theorem

(defthm |(< (/ x) c) positive c --- present in goal|
  (implies (and (syntaxp (numeric-constant-p c))
      (real/rationalp c)
      (< 0 c)
      (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (let ((parity (present-in-goal `(< ,X ,C) mfc state)))
          (cond ((eq parity 'positive) t)
            ((eq parity 'negative) (not (proveably-integer 'x `((x . ,X)) mfc state)))
            (t nil))))
      (syntaxp (mostly-divisive-factors-p x mfc state))
      (real/rationalp x))
    (equal (< x c) (or (<= (/ x) 0) (< (/ c) (/ x))))))

|(< (/ x) c) positive c --- obj t or nil|theorem

(defthm |(< (/ x) c) positive c --- obj t or nil|
  (implies (and (syntaxp (numeric-constant-p c))
      (real/rationalp c)
      (< 0 c)
      (syntaxp (or (eq (mfc-obj x mfc state) 't)
          (and (eq (mfc-obj x mfc state) 'nil)
            (not (proveably-integer 'x `((x . ,X)) mfc state)))))
      (syntaxp (mostly-divisive-factors-p x mfc state))
      (real/rationalp x))
    (equal (< x c) (or (<= (/ x) 0) (< (/ c) (/ x))))))

|(< c (/ x)) positive c --- present in goal|theorem

(defthm |(< c (/ x)) positive c --- present in goal|
  (implies (and (syntaxp (numeric-constant-p c))
      (real/rationalp c)
      (< 0 c)
      (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (let ((parity (present-in-goal `(< ,C ,X) mfc state)))
          (cond ((eq parity 'positive) t)
            ((eq parity 'negative) (not (proveably-integer 'x `((x . ,X)) mfc state)))
            (t nil))))
      (syntaxp (mostly-divisive-factors-p x mfc state))
      (real/rationalp x))
    (equal (< c x) (and (< 0 (/ x)) (< (/ x) (/ c))))))

|(< c (/ x)) positive c --- obj t or nil|theorem

(defthm |(< c (/ x)) positive c --- obj t or nil|
  (implies (and (syntaxp (numeric-constant-p c))
      (real/rationalp c)
      (< 0 c)
      (syntaxp (or (eq (mfc-obj x mfc state) 't)
          (and (eq (mfc-obj x mfc state) 'nil)
            (not (proveably-integer 'x `((x . ,X)) mfc state)))))
      (syntaxp (mostly-divisive-factors-p x mfc state))
      (real/rationalp x))
    (equal (< c x) (and (< 0 (/ x)) (< (/ x) (/ c))))))

|(< c (/ x)) negative c --- present in goal|theorem

(defthm |(< c (/ x)) negative c --- present in goal|
  (implies (and (syntaxp (numeric-constant-p c))
      (real/rationalp c)
      (< c 0)
      (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (let ((parity (present-in-goal `(< ,C ,X) mfc state)))
          (cond ((eq parity 'positive) t)
            ((eq parity 'negative) (not (proveably-integer 'x `((x . ,X)) mfc state)))
            (t nil))))
      (syntaxp (mostly-divisive-factors-p x mfc state))
      (real/rationalp x))
    (equal (< c x) (or (<= 0 (/ x)) (< (/ x) (/ c))))))

|(< c (/ x)) negative c --- obj t or nil|theorem

(defthm |(< c (/ x)) negative c --- obj t or nil|
  (implies (and (syntaxp (numeric-constant-p c))
      (real/rationalp c)
      (< c 0)
      (syntaxp (or (eq (mfc-obj x mfc state) 't)
          (and (eq (mfc-obj x mfc state) 'nil)
            (not (proveably-integer 'x `((x . ,X)) mfc state)))))
      (syntaxp (mostly-divisive-factors-p x mfc state))
      (real/rationalp x))
    (equal (< c x) (or (<= 0 (/ x)) (< (/ x) (/ c))))))

|(< (- x) (- y))|theorem

(defthm |(< (- x) (- y))|
  (implies (and (syntaxp (mostly-negative-addends-p x mfc state))
      (syntaxp (mostly-negative-addends-p y mfc state)))
    (equal (< x y) (< (- y) (- x)))))

|(< (/ x) (/ y))|theorem

(defthm |(< (/ x) (/ y))|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (mostly-divisive-factors-p x mfc state))
      (syntaxp (mostly-divisive-factors-p y mfc state))
      (syntaxp (let ((parity (present-in-goal `(< ,X ,Y) mfc state)))
          (cond ((eq parity 'positive) t)
            ((eq parity 'negative) (and (not (proveably-integer 'x `((x . ,X)) mfc state))
                (not (proveably-integer 'y `((y . ,Y)) mfc state))))
            (t nil))))
      (real/rationalp x)
      (real/rationalp y))
    (equal (< x y)
      (cond ((and (< 0 x) (< 0 y)) (< (/ y) (/ x)))
        ((and (< x 0) (< y 0)) (< (/ y) (/ x)))
        (t (< (/ x) (/ y))))))
  :hints (("Goal" :in-theory (enable normalize-<-/-to-*-1
       normalize-<-/-to-*-2
       normalize-<-/-to-*-3-2
       normalize-<-/-to-*-3-4))))

|(equal x (/ y))|theorem

(defthm |(equal x (/ y))|
  (implies (and (acl2-numberp x) (acl2-numberp y) (equal (* x y) 1))
    (equal (equal x (/ y)) t))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1))))

|(not (equal x (/ y)))|theorem

(defthm |(not (equal x (/ y)))|
  (implies (and (acl2-numberp x)
      (acl2-numberp y)
      (not (equal x 0))
      (not (equal y 0))
      (not (equal (* x y) 1)))
    (equal (equal x (/ y)) nil))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1 1))))

|(equal x (- (/ y)))|theorem

(defthm |(equal x (- (/ y)))|
  (implies (and (acl2-numberp x) (acl2-numberp y) (equal (* x y) -1))
    (equal (equal x (- (/ y))) t))
  :hints (("Goal" :use (:instance |(equal c (/ x))| (c x) (x (- (/ y))))))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1))))

|(not (equal x (- (/ y))))|theorem

(defthm |(not (equal x (- (/ y))))|
  (implies (and (acl2-numberp x)
      (acl2-numberp y)
      (not (equal x 0))
      (not (equal y 0))
      (not (equal (* x y) -1)))
    (equal (equal x (- (/ y))) nil))
  :hints (("Goal" :use (:instance |(equal c (/ x))| (c x) (x (- (/ y))))))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1 1))))

|(equal (* x (/ y)) 1)|theorem

(defthm |(equal (* x (/ y)) 1)|
  (implies (and (acl2-numberp x)
      (acl2-numberp y)
      (not (equal x 0))
      (equal x y))
    (equal (equal (* x (/ y)) 1) t))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(not (equal (* x (/ y)) 1))|theorem

(defthm |(not (equal (* x (/ y)) 1))|
  (implies (and (acl2-numberp x) (acl2-numberp y) (not (equal x y)))
    (equal (equal (* x (/ y)) 1) nil))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1))))

|(equal (* (/ x) y) 1)|theorem

(defthm |(equal (* (/ x) y) 1)|
  (implies (and (acl2-numberp x)
      (acl2-numberp y)
      (not (equal x 0))
      (equal x y))
    (equal (equal (* (/ x) y) 1) t))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(not (equal (* (/ x) y) 1))|theorem

(defthm |(not (equal (* (/ x) y) 1))|
  (implies (and (acl2-numberp x) (acl2-numberp y) (not (equal x y)))
    (equal (equal (* (/ x) y) 1) nil))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1))))

|(equal (* x (/ y)) -1)|theorem

(defthm |(equal (* x (/ y)) -1)|
  (implies (and (acl2-numberp x)
      (acl2-numberp y)
      (not (equal x 0))
      (equal x (- y)))
    (equal (equal (* x (/ y)) -1) t))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(not (equal (* x (/ y)) -1))|theorem

(defthm |(not (equal (* x (/ y)) -1))|
  (implies (and (acl2-numberp x)
      (acl2-numberp y)
      (not (equal x (- y))))
    (equal (equal (* x (/ y)) -1) nil))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1))))

|(equal (* (/ x) y) -1)|theorem

(defthm |(equal (* (/ x) y) -1)|
  (implies (and (acl2-numberp x)
      (acl2-numberp y)
      (not (equal x 0))
      (equal x (- y)))
    (equal (equal (* (/ x) y) -1) t))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(not (equal (* (/ x) y) -1))|theorem

(defthm |(not (equal (* (/ x) y) -1))|
  (implies (and (acl2-numberp x)
      (acl2-numberp y)
      (not (equal x (- y))))
    (equal (equal (* (/ x) y) -1) nil))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1))))

|(< x (/ y)) with (< 0 y)|theorem

(defthm |(< x (/ y)) with (< 0 y)|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (< 0 y)
      (< (* x y) 1))
    (< x (/ y)))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(<= x (/ y)) with (< 0 y)|theorem

(defthm |(<= x (/ y)) with (< 0 y)|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (< 0 y)
      (<= (* x y) 1))
    (<= x (/ y)))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(< x (/ y)) with (< y 0)|theorem

(defthm |(< x (/ y)) with (< y 0)|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (< y 0)
      (< 1 (* x y)))
    (< x (/ y)))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(<= x (/ y)) with (< y 0)|theorem

(defthm |(<= x (/ y)) with (< y 0)|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (< y 0)
      (<= 1 (* x y)))
    (<= x (/ y)))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(< (/ x) y) with (< 0 x)|theorem

(defthm |(< (/ x) y) with (< 0 x)|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (< 0 x)
      (< 1 (* x y)))
    (< (/ x) y))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(<= (/ x) y) with (< 0 x)|theorem

(defthm |(<= (/ x) y) with (< 0 x)|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (< 0 x)
      (<= 1 (* x y)))
    (<= (/ x) y))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(< (/ x) y) with (< x 0)|theorem

(defthm |(< (/ x) y) with (< x 0)|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (< x 0)
      (< (* x y) 1))
    (< (/ x) y))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(<= (/ x) y) with (< x 0)|theorem

(defthm |(<= (/ x) y) with (< x 0)|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (< x 0)
      (<= (* x y) 1))
    (<= (/ x) y))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(< 1 (* x (/ y))) with (< 0 y)|theorem

(defthm |(< 1 (* x (/ y))) with (< 0 y)|
  (implies (and (real/rationalp x) (real/rationalp y) (< 0 y) (< y x))
    (< 1 (* x (/ y))))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(<= 1 (* x (/ y))) with (< 0 y)|theorem

(defthm |(<= 1 (* x (/ y))) with (< 0 y)|
  (implies (and (real/rationalp x) (real/rationalp y) (< 0 y) (<= y x))
    (<= 1 (* x (/ y))))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(< 1 (* x (/ y))) with (< y 0)|theorem

(defthm |(< 1 (* x (/ y))) with (< y 0)|
  (implies (and (real/rationalp x) (real/rationalp y) (< y 0) (< x y))
    (< 1 (* x (/ y))))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(<= 1 (* x (/ y))) with (< y 0)|theorem

(defthm |(<= 1 (* x (/ y))) with (< y 0)|
  (implies (and (real/rationalp x) (real/rationalp y) (< y 0) (<= x y))
    (<= 1 (* x (/ y))))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(< 1 (* (/ x) y)) with (< 0 x)|theorem

(defthm |(< 1 (* (/ x) y)) with (< 0 x)|
  (implies (and (real/rationalp x) (real/rationalp y) (< 0 x) (< x y))
    (< 1 (* (/ x) y)))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(<= 1 (* (/ x) y)) with (< 0 x)|theorem

(defthm |(<= 1 (* (/ x) y)) with (< 0 x)|
  (implies (and (real/rationalp x) (real/rationalp y) (< 0 x) (<= x y))
    (<= 1 (* (/ x) y)))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(< 1 (* (/ x) y)) with (< x 0)|theorem

(defthm |(< 1 (* (/ x) y)) with (< x 0)|
  (implies (and (real/rationalp x) (real/rationalp y) (< x 0) (< y x))
    (< 1 (* (/ x) y)))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(<= 1 (* (/ x) y)) with (< x 0)|theorem

(defthm |(<= 1 (* (/ x) y)) with (< x 0)|
  (implies (and (real/rationalp x) (real/rationalp y) (< x 0) (<= y x))
    (<= 1 (* (/ x) y)))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(< (* x (/ y)) 1) with (< 0 y)|theorem

(defthm |(< (* x (/ y)) 1) with (< 0 y)|
  (implies (and (real/rationalp x) (real/rationalp y) (< 0 y) (< x y))
    (< (* x (/ y)) 1))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(<= (* x (/ y)) 1) with (< 0 y)|theorem

(defthm |(<= (* x (/ y)) 1) with (< 0 y)|
  (implies (and (real/rationalp x) (real/rationalp y) (< 0 y) (<= x y))
    (<= (* x (/ y)) 1))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(< (* x (/ y)) 1) with (< y 0)|theorem

(defthm |(< (* x (/ y)) 1) with (< y 0)|
  (implies (and (real/rationalp x) (real/rationalp y) (< y 0) (< y x))
    (< (* x (/ y)) 1))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(<= (* x (/ y)) 1) with (< y 0)|theorem

(defthm |(<= (* x (/ y)) 1) with (< y 0)|
  (implies (and (real/rationalp x) (real/rationalp y) (< y 0) (<= y x))
    (<= (* x (/ y)) 1))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(< (* (/ x) y) 1) with (< 0 x)|theorem

(defthm |(< (* (/ x) y) 1) with (< 0 x)|
  (implies (and (real/rationalp x) (real/rationalp y) (< 0 x) (< y x))
    (< (* (/ x) y) 1))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(<= (* (/ x) y) 1) with (< 0 x)|theorem

(defthm |(<= (* (/ x) y) 1) with (< 0 x)|
  (implies (and (real/rationalp x) (real/rationalp y) (< 0 x) (<= y x))
    (<= (* (/ x) y) 1))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(< (* (/ x) y) 1) with (< x 0)|theorem

(defthm |(< (* (/ x) y) 1) with (< x 0)|
  (implies (and (real/rationalp x) (real/rationalp y) (< x 0) (< x y))
    (< (* (/ x) y) 1))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(<= (* (/ x) y) 1) with (< x 0)|theorem

(defthm |(<= (* (/ x) y) 1) with (< x 0)|
  (implies (and (real/rationalp x) (real/rationalp y) (< x 0) (<= x y))
    (<= (* (/ x) y) 1))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(< -1 (* x (/ y))) with (< 0 y)|theorem

(defthm |(< -1 (* x (/ y))) with (< 0 y)|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (< 0 y)
      (< (- y) x))
    (< -1 (* x (/ y))))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(<= -1 (* x (/ y))) with (< 0 y)|theorem

(defthm |(<= -1 (* x (/ y))) with (< 0 y)|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (< 0 y)
      (<= (- y) x))
    (<= -1 (* x (/ y))))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(< -1 (* x (/ y))) with (< y 0)|theorem

(defthm |(< -1 (* x (/ y))) with (< y 0)|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (< y 0)
      (< x (- y)))
    (< -1 (* x (/ y))))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(<= -1 (* x (/ y))) with (< y 0)|theorem

(defthm |(<= -1 (* x (/ y))) with (< y 0)|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (< y 0)
      (<= x (- y)))
    (<= -1 (* x (/ y))))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(< -1 (* (/ x) y)) with (< 0 x)|theorem

(defthm |(< -1 (* (/ x) y)) with (< 0 x)|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (< 0 x)
      (< (- x) y))
    (< -1 (* (/ x) y)))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(<= -1 (* (/ x) y)) with (< 0 x)|theorem

(defthm |(<= -1 (* (/ x) y)) with (< 0 x)|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (< 0 x)
      (<= (- x) y))
    (<= -1 (* (/ x) y)))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(< -1 (* (/ x) y)) with (< x 0)|theorem

(defthm |(< -1 (* (/ x) y)) with (< x 0)|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (< x 0)
      (< y (- x)))
    (< -1 (* (/ x) y)))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(<= -1 (* (/ x) y)) with (< x 0)|theorem

(defthm |(<= -1 (* (/ x) y)) with (< x 0)|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (< x 0)
      (<= y (- x)))
    (<= -1 (* (/ x) y)))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(< (* x (/ y)) -1) with (< 0 y)|theorem

(defthm |(< (* x (/ y)) -1) with (< 0 y)|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (< 0 y)
      (< x (- y)))
    (< (* x (/ y)) -1))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(<= (* x (/ y)) -1) with (< 0 y)|theorem

(defthm |(<= (* x (/ y)) -1) with (< 0 y)|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (< 0 y)
      (<= x (- y)))
    (<= (* x (/ y)) -1))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(< (* x (/ y)) -1) with (< y 0)|theorem

(defthm |(< (* x (/ y)) -1) with (< y 0)|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (< y 0)
      (< (- y) x))
    (< (* x (/ y)) -1))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(<= (* x (/ y)) -1) with (< y 0)|theorem

(defthm |(<= (* x (/ y)) -1) with (< y 0)|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (< y 0)
      (<= (- y) x))
    (<= (* x (/ y)) -1))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(< (* (/ x) y) -1) with (< 0 x)|theorem

(defthm |(< (* (/ x) y) -1) with (< 0 x)|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (< 0 x)
      (< y (- x)))
    (< (* (/ x) y) -1))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(<= (* (/ x) y) -1) with (< 0 x)|theorem

(defthm |(<= (* (/ x) y) -1) with (< 0 x)|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (< 0 x)
      (<= y (- x)))
    (<= (* (/ x) y) -1))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(< (* (/ x) y) -1) with (< x 0)|theorem

(defthm |(< (* (/ x) y) -1) with (< x 0)|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (< x 0)
      (< (- x) y))
    (< (* (/ x) y) -1))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

|(<= (* (/ x) y) -1) with (< x 0)|theorem

(defthm |(<= (* (/ x) y) -1) with (< x 0)|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (< x 0)
      (<= (- x) y))
    (<= (* (/ x) y) -1))
  :rule-classes ((:rewrite :backchain-limit-lst (2 2 1 1))))

local

(local (defthm equal-to-iff
    (equal (equal (< a b) (< x y)) (iff (< a b) (< x y)))))

|(equal (+ (- c) x) y)|theorem

(defthm |(equal (+ (- c) x) y)|
  (implies (and (syntaxp (quotep c))
      (acl2-numberp c)
      (< c 0)
      (syntaxp (simplify-ok-p `(equal (binary-+ ,C ,X) ,Y)
          '(equal x (binary-+ (unary-- c) y))
          `((x . ,X) (y . ,Y) (c . ,C))
          mfc
          state))
      (acl2-numberp x)
      (acl2-numberp y))
    (equal (equal (+ c x) y) (equal x (+ (- c) y)))))

|(< (+ (- c) x) y)|theorem

(defthm |(< (+ (- c) x) y)|
  (implies (and (syntaxp (quotep c))
      (acl2-numberp c)
      (< c 0)
      (syntaxp (simplify-ok-p `(< (binary-+ ,C ,X) ,Y)
          '(< x (binary-+ (unary-- c) y))
          `((x . ,X) (y . ,Y) (c . ,C))
          mfc
          state))
      (acl2-numberp x)
      (acl2-numberp y))
    (equal (< (+ c x) y) (< x (+ (- c) y)))))

|(< y (+ (- c) x))|theorem

(defthm |(< y (+ (- c) x))|
  (implies (and (syntaxp (quotep c))
      (acl2-numberp c)
      (< c 0)
      (syntaxp (simplify-ok-p `(< ,Y (binary-+ ,C ,X))
          '(< (binary-+ (unary-- c) y) x)
          `((x . ,X) (y . ,Y) (c . ,C))
          mfc
          state))
      (acl2-numberp x)
      (acl2-numberp y))
    (equal (< y (+ c x)) (< (+ (- c) y) x))))

find-constant-addendfunction

(defun find-constant-addend
  (lhs rhs)
  (cond ((and (eq (fn-symb lhs) 'binary-+)
       (eq (fn-symb rhs) 'binary-+)
       (numeric-constant-p (arg1 lhs))
       (numeric-constant-p (arg1 rhs))) (let ((c (unquote (arg1 lhs))) (d (unquote (arg1 rhs))))
        (cond ((eql c 0) nil)
          ((eql d 0) nil)
          ((< c d) `((c . ,(KWOTE (- C)))))
          (t `((c . ,(KWOTE (- D))))))))
    ((and (eq (fn-symb rhs) 'binary-+)
       (numeric-constant-p lhs)
       (numeric-constant-p (arg1 rhs))) (let ((c (unquote lhs)) (d (unquote (arg1 rhs))))
        (cond ((eql c 0) `((c . ,(KWOTE (- D)))))
          ((eql d 0) nil)
          ((< c d) `((c . ,(KWOTE (- C)))))
          (t `((c . ,(KWOTE (- D))))))))
    ((and (eq (fn-symb lhs) 'binary-+)
       (numeric-constant-p (arg1 lhs))
       (numeric-constant-p rhs)) (let ((c (unquote (arg1 lhs))) (d (unquote rhs)))
        (cond ((eql c 0) nil)
          ((eql d 0) `((c . ,(KWOTE (- C)))))
          ((< c d) `((c . ,(KWOTE (- C)))))
          (t `((c . ,(KWOTE (- D))))))))
    (t nil)))

reduce-additive-constant-equaltheorem

(defthm reduce-additive-constant-equal
  (implies (and (syntaxp (in-term-order-+ lhs mfc state))
      (syntaxp (in-term-order-+ rhs mfc state))
      (bind-free (find-constant-addend lhs rhs) (c))
      (not (equal c 0))
      (syntaxp (simplify-ok-p `(equal ,LHS ,RHS)
          '(equal (binary-+ c lhs) (binary-+ c rhs))
          `((lhs . ,LHS) (rhs . ,RHS) (c . ,C))
          mfc
          state))
      (acl2-numberp lhs)
      (acl2-numberp rhs)
      (acl2-numberp c))
    (equal (equal lhs rhs) (equal (+ c lhs) (+ c rhs)))))

reduce-additive-constant-<theorem

(defthm reduce-additive-constant-<
  (implies (and (syntaxp (in-term-order-+ lhs mfc state))
      (syntaxp (in-term-order-+ rhs mfc state))
      (bind-free (find-constant-addend lhs rhs) (c))
      (not (equal c 0))
      (syntaxp (simplify-ok-p `(< ,LHS ,RHS)
          '(< (binary-+ c lhs) (binary-+ c rhs))
          `((lhs . ,LHS) (rhs . ,RHS) (c . ,C))
          mfc
          state))
      (acl2-numberp lhs)
      (acl2-numberp rhs)
      (acl2-numberp c))
    (equal (< lhs rhs) (< (+ c lhs) (+ c rhs)))))

find-constant-factor-equalfunction

(defun find-constant-factor-equal
  (lhs rhs)
  (cond ((and (eq (fn-symb lhs) 'binary-*)
       (eq (fn-symb rhs) 'binary-*)
       (numeric-constant-p (arg1 lhs))
       (numeric-constant-p (arg1 rhs))) (let ((c (unquote (arg1 lhs))) (d (unquote (arg1 rhs))))
        (cond ((or (eql c 0) (eql (abs c) 1)) `((c . ,(KWOTE (/ D)))))
          ((or (eql d 0) (eql (abs d) 1)) `((c . ,(KWOTE (/ C)))))
          ((< c d) `((c . ,(KWOTE (/ C)))))
          (t `((c . ,(KWOTE (/ D))))))))
    ((and (eq (fn-symb rhs) 'binary-*)
       (numeric-constant-p lhs)
       (numeric-constant-p (arg1 rhs))) (let ((c (unquote lhs)) (d (unquote (arg1 rhs))))
        (cond ((or (eql c 0) (eql (abs c) 1)) `((c . ,(KWOTE (/ D)))))
          ((or (eql d 0) (eql (abs d) 1)) `((c . ,(KWOTE (/ C)))))
          ((< c d) `((c . ,(KWOTE (/ C)))))
          (t `((c . ,(KWOTE (/ D))))))))
    ((and (eq (fn-symb lhs) 'binary-*)
       (numeric-constant-p (arg1 lhs))
       (numeric-constant-p rhs)) (let ((c (unquote (arg1 lhs))) (d (unquote rhs)))
        (cond ((or (eql c 0) (eql (abs c) 1)) `((c . ,(KWOTE (/ D)))))
          ((or (eql d 0) (eql (abs d) 1)) `((c . ,(KWOTE (/ C)))))
          ((< c d) `((c . ,(KWOTE (/ C)))))
          (t `((c . ,(KWOTE (/ D))))))))
    ((and (eq (fn-symb rhs) 'binary-*)
       (numeric-constant-p (arg1 rhs))
       (not (eq (fn-symb (arg2 rhs)) 'binary-*))
       (eq (fn-symb lhs) 'binary-+)) `((c . ,(KWOTE (/ (UNQUOTE (ARG1 LHS)))))))
    ((and (eq (fn-symb lhs) 'binary-*)
       (numeric-constant-p (arg1 lhs))
       (not (eq (fn-symb (arg2 lhs)) 'binary-*))
       (eq (fn-symb rhs) 'binary-+)) `((c . ,(KWOTE (/ (UNQUOTE (ARG1 RHS)))))))
    ((and (eq (fn-symb rhs) 'binary-+)
       (eq (fn-symb lhs) 'binary-+)) nil)
    (t nil)))

find-rational-constant-factor-<function

(defun find-rational-constant-factor-<
  (lhs rhs)
  (cond ((and (eq (fn-symb lhs) 'binary-*)
       (eq (fn-symb rhs) 'binary-*)
       (rational-constant-p (arg1 lhs))
       (rational-constant-p (arg1 rhs))) (let ((c (unquote (arg1 lhs))) (d (unquote (arg1 rhs))))
        (cond ((or (eql c 0) (eql (abs c) 1)) `((c . ,(KWOTE (/ D)))))
          ((or (eql d 0) (eql (abs d) 1)) `((c . ,(KWOTE (/ C)))))
          ((< c d) `((c . ,(KWOTE (/ C)))))
          (t `((c . ,(KWOTE (/ D))))))))
    ((and (eq (fn-symb rhs) 'binary-*)
       (rational-constant-p lhs)
       (rational-constant-p (arg1 rhs))) (let ((c (unquote lhs)) (d (unquote (arg1 rhs))))
        (cond ((or (eql c 0) (eql (abs c) 1)) `((c . ,(KWOTE (/ D)))))
          ((or (eql d 0) (eql (abs d) 1)) `((c . ,(KWOTE (/ C)))))
          ((< c d) `((c . ,(KWOTE (/ C)))))
          (t `((c . ,(KWOTE (/ D))))))))
    ((and (eq (fn-symb lhs) 'binary-*)
       (rational-constant-p (arg1 lhs))
       (rational-constant-p rhs)) (let ((c (unquote (arg1 lhs))) (d (unquote rhs)))
        (cond ((or (eql c 0) (eql (abs c) 1)) `((c . ,(KWOTE (/ D)))))
          ((or (eql d 0) (eql (abs d) 1)) `((c . ,(KWOTE (/ C)))))
          ((< c d) `((c . ,(KWOTE (/ C)))))
          (t `((c . ,(KWOTE (/ D))))))))
    ((and (eq (fn-symb rhs) 'binary-*)
       (rational-constant-p (arg1 rhs))
       (not (eq (fn-symb (arg2 rhs)) 'binary-*))
       (eq (fn-symb lhs) 'binary-+)) nil)
    ((and (eq (fn-symb lhs) 'binary-*)
       (rational-constant-p (arg1 lhs))
       (not (eq (fn-symb (arg2 lhs)) 'binary-*))
       (eq (fn-symb rhs) 'binary-+)) nil)
    ((and (eq (fn-symb rhs) 'binary-+)
       (eq (fn-symb lhs) 'binary-+)) nil)
    (t nil)))

find-constant-factor-<function

(defun find-constant-factor-<
  (lhs rhs)
  (cond ((and (eq (fn-symb lhs) 'binary-*)
       (eq (fn-symb rhs) 'binary-*)
       (numeric-constant-p (arg1 lhs))
       (numeric-constant-p (arg1 rhs))) (let ((c (unquote (arg1 lhs))) (d (unquote (arg1 rhs))))
        (cond ((or (eql c 0) (eql (abs c) 1)) `((c . ,(KWOTE (/ D)))))
          ((or (eql d 0) (eql (abs d) 1)) `((c . ,(KWOTE (/ C)))))
          ((< c d) `((c . ,(KWOTE (/ C)))))
          (t `((c . ,(KWOTE (/ D))))))))
    ((and (eq (fn-symb rhs) 'binary-*)
       (numeric-constant-p lhs)
       (numeric-constant-p (arg1 rhs))) (let ((c (unquote lhs)) (d (unquote (arg1 rhs))))
        (cond ((or (eql c 0) (eql (abs c) 1)) `((c . ,(KWOTE (/ D)))))
          ((or (eql d 0) (eql (abs d) 1)) `((c . ,(KWOTE (/ C)))))
          ((< c d) `((c . ,(KWOTE (/ C)))))
          (t `((c . ,(KWOTE (/ D))))))))
    ((and (eq (fn-symb lhs) 'binary-*)
       (numeric-constant-p (arg1 lhs))
       (numeric-constant-p rhs)) (let ((c (unquote (arg1 lhs))) (d (unquote rhs)))
        (cond ((or (eql c 0) (eql (abs c) 1)) `((c . ,(KWOTE (/ D)))))
          ((or (eql d 0) (eql (abs d) 1)) `((c . ,(KWOTE (/ C)))))
          ((< c d) `((c . ,(KWOTE (/ C)))))
          (t `((c . ,(KWOTE (/ D))))))))
    ((and (eq (fn-symb rhs) 'binary-*)
       (numeric-constant-p (arg1 rhs))
       (not (eq (fn-symb (arg2 rhs)) 'binary-*))
       (eq (fn-symb lhs) 'binary-+)) nil)
    ((and (eq (fn-symb lhs) 'binary-*)
       (numeric-constant-p (arg1 lhs))
       (not (eq (fn-symb (arg2 lhs)) 'binary-*))
       (eq (fn-symb rhs) 'binary-+)) nil)
    ((and (eq (fn-symb rhs) 'binary-+)
       (eq (fn-symb lhs) 'binary-+)) nil)
    (t nil)))

reduce-multiplicative-constant-equaltheorem

(defthm reduce-multiplicative-constant-equal
  (implies (and (syntaxp (in-term-order-* lhs mfc state))
      (syntaxp (in-term-order-* rhs mfc state))
      (bind-free (find-constant-factor-equal lhs rhs) (c))
      (not (equal c 0))
      (not (equal (abs c) 1))
      (syntaxp (simplify-ok-p `(equal ,LHS ,RHS)
          '(equal (binary-* c lhs) (binary-* c rhs))
          `((lhs . ,LHS) (rhs . ,RHS) (c . ,C))
          mfc
          state))
      (acl2-numberp lhs)
      (acl2-numberp rhs)
      (acl2-numberp c))
    (equal (equal lhs rhs) (equal (* c lhs) (* c rhs)))))

reduce-rational-multiplicative-constant-<theorem

(defthm reduce-rational-multiplicative-constant-<
  (implies (and (syntaxp (in-term-order-* lhs mfc state))
      (syntaxp (in-term-order-* rhs mfc state))
      (bind-free (find-rational-constant-factor-< lhs rhs) (c))
      (not (equal c 0))
      (not (equal (abs c) 1))
      (syntaxp (simplify-ok-p `(< ,LHS ,RHS)
          '(< (binary-* c lhs) (binary-* c rhs))
          `((lhs . ,LHS) (rhs . ,RHS) (c . ,C))
          mfc
          state))
      (acl2-numberp lhs)
      (acl2-numberp rhs)
      (real/rationalp c))
    (equal (< lhs rhs)
      (if (< 0 c)
        (< (* c lhs) (* c rhs))
        (< (* c rhs) (* c lhs))))))

reduce-multiplicative-constant-<theorem

(defthm reduce-multiplicative-constant-<
  (implies (and (syntaxp (in-term-order-* lhs mfc state))
      (syntaxp (in-term-order-* rhs mfc state))
      (bind-free (find-constant-factor-< lhs rhs) (c))
      (not (equal c 0))
      (not (equal (abs c) 1))
      (syntaxp (simplify-ok-p `(< ,LHS ,RHS)
          '(< (binary-* c lhs) (binary-* c rhs))
          `((lhs . ,LHS) (rhs . ,RHS) (c . ,C))
          mfc
          state))
      (real/rationalp lhs)
      (real/rationalp rhs)
      (acl2-numberp c))
    (equal (< lhs rhs)
      (if (< 0 c)
        (< (* c lhs) (* c rhs))
        (< (* c rhs) (* c lhs)))))
  :hints (("Goal" :use (:instance big-helper-2))))

|(< (+ c/d x) y)|theorem

(defthm |(< (+ c/d x) y)|
  (implies (and (syntaxp (rational-constant-p c))
      (syntaxp (not (integer-constant-p c)))
      (syntaxp (simplify-ok-p `(< (binary-+ ,C ,X) ,Y)
          '(< (binary-* (denominator c) (binary-+ c x))
            (binary-* (denominator c) y))
          `((x . ,X) (y . ,Y) (c . ,C))
          mfc
          state))
      (real/rationalp c)
      (not (equal c 0))
      (acl2-numberp y))
    (equal (< (+ c x) y)
      (< (* (denominator c) (+ c x)) (* (denominator c) y))))
  :hints (("Goal" :in-theory (disable *-r-denominator-r-pass1))))

|(< x (+ c/d y))|theorem

(defthm |(< x (+ c/d y))|
  (implies (and (syntaxp (rational-constant-p c))
      (syntaxp (not (integer-constant-p c)))
      (syntaxp (simplify-ok-p `(< ,X (binary-+ ,C ,Y))
          '(< (binary-* (denominator c) x)
            (binary-* (denominator c) (binary-+ c y)))
          `((x . ,X) (y . ,Y) (c . ,C))
          mfc
          state))
      (real/rationalp c)
      (not (equal c 0))
      (acl2-numberp x))
    (equal (< x (+ c y))
      (< (* (denominator c) x) (* (denominator c) (+ c y)))))
  :hints (("Goal" :in-theory (disable *-r-denominator-r-pass1))))

|(equal (* x y) 0)|theorem

(defthm |(equal (* x y) 0)|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (present-in-goal `(equal (binary-* ,X ,Y) '0) mfc state))
      (acl2-numberp x)
      (acl2-numberp y))
    (equal (equal (* x y) 0) (or (equal x 0) (equal y 0)))))

productfunction

(defun product
  (factors)
  (declare (xargs :guard t))
  (cond ((atom factors) nil)
    ((atom (cdr factors)) (car factors))
    (t `(binary-* ,(CAR FACTORS) ,(PRODUCT (CDR FACTORS))))))

find-rational-factor-and-remainder-1function

(defun find-rational-factor-and-remainder-1
  (x rem mfc state)
  (declare (xargs :guard (true-listp rem)))
  (cond ((not (eq (fn-symb x) 'binary-*)) nil)
    ((proveably-real/rational 'x `((x . ,(ARG1 X))) mfc state) `((y . ,(ARG1 X)) (z . ,(PRODUCT (REVERSE (CONS (ARG2 X) REM))))))
    ((eq (fn-symb (arg2 x)) 'binary-*) (find-rational-factor-and-remainder-1 (arg2 x)
        (cons (arg1 x) rem)
        mfc
        state))
    ((proveably-real/rational 'x `((x . ,(ARG2 X))) mfc state) `((y . ,(ARG2 X)) (z . ,(PRODUCT (REVERSE (CONS (ARG1 X) REM))))))
    (t nil)))

find-rational-factor-and-remainderfunction

(defun find-rational-factor-and-remainder
  (x mfc state)
  (declare (xargs :guard t))
  (find-rational-factor-and-remainder-1 x nil mfc state))

|(< (* x y) 0)|theorem

(defthm |(< (* x y) 0)|
  (implies (and (syntaxp (eq (fn-symb x) 'binary-*))
      (syntaxp (in-term-order-* x mfc state))
      (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (present-in-goal `(< ,X '0) mfc state))
      (bind-free (find-rational-factor-and-remainder x mfc state)
        (y z))
      (equal x (* y z))
      (real/rationalp y)
      (acl2-numberp z))
    (equal (< x 0)
      (cond ((equal y 0) nil)
        ((equal z 0) nil)
        ((< 0 y) (< z 0))
        ((< y 0) (< 0 z)))))
  :hints (("Goal" :use ((:instance big-helper-1 (y z) (z y)))
     :in-theory (disable big-helper-1))))

|(< 0 (* x y))|theorem

(defthm |(< 0 (* x y))|
  (implies (and (syntaxp (eq (fn-symb x) 'binary-*))
      (syntaxp (in-term-order-* x mfc state))
      (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (present-in-goal `(< '0 ,X) mfc state))
      (bind-free (find-rational-factor-and-remainder x mfc state)
        (y z))
      (equal x (* y z))
      (real/rationalp y)
      (acl2-numberp z))
    (equal (< 0 x)
      (cond ((equal y 0) nil)
        ((equal z 0) nil)
        ((< 0 y) (< 0 z))
        ((< y 0) (< z 0)))))
  :hints (("Goal" :use ((:instance big-helper-1 (y z) (z y)))
     :in-theory (disable big-helper-1))))

|(< (* x y) 0) rationalp (* x y)|theorem

(defthm |(< (* x y) 0) rationalp (* x y)|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (present-in-goal `(< (binary-* ,X ,Y) '0) mfc state))
      (acl2-numberp x)
      (real/rationalp (* x y)))
    (equal (< (* x y) 0)
      (cond ((equal y 0) nil)
        ((equal x 0) nil)
        ((< 0 y) (< (/ x) 0))
        ((< y 0) (< 0 (/ x))))))
  :hints (("Goal" :use (:instance big-helper-2 (lhs (* x y)) (rhs 0) (c (/ x))))))

|(< 0 (* x y)) rationalp (* x y)|theorem

(defthm |(< 0 (* x y)) rationalp (* x y)|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (present-in-goal `(< '0 (binary-* ,X ,Y)) mfc state))
      (acl2-numberp x)
      (real/rationalp (* x y)))
    (equal (< 0 (* x y))
      (cond ((equal y 0) nil)
        ((equal x 0) nil)
        ((< 0 y) (< 0 (/ x)))
        ((< y 0) (< (/ x) 0)))))
  :hints (("Goal" :use (:instance big-helper-2 (lhs 0) (rhs (* x y)) (c (/ x))))))

|(< (* x (/ y)) 0) rationalp (* x (/ y))|theorem

(defthm |(< (* x (/ y)) 0) rationalp (* x (/ y))|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (present-in-goal `(< (binary-* ,X (unary-/ ,Y)) '0)
          mfc
          state))
      (acl2-numberp y)
      (real/rationalp (* x (/ y))))
    (equal (< (* x (/ y)) 0)
      (cond ((equal y 0) nil)
        ((equal x 0) nil)
        ((< 0 y) (< x 0))
        ((< y 0) (< 0 x)))))
  :hints (("Goal" :use (:instance big-helper-2 (lhs (* x (/ y))) (rhs 0) (c y)))))

|(< 0 (* x (/ y))) rationalp (* x (/ y))|theorem

(defthm |(< 0 (* x (/ y))) rationalp (* x (/ y))|
  (implies (and (syntaxp (rewriting-goal-literal x mfc state))
      (syntaxp (present-in-goal `(< '0 (binary-* ,X (unary-/ ,Y)))
          mfc
          state))
      (acl2-numberp y)
      (real/rationalp (* x (/ y))))
    (equal (< 0 (* x (/ y)))
      (cond ((equal y 0) nil)
        ((equal x 0) nil)
        ((< 0 y) (< 0 x))
        ((< y 0) (< x 0)))))
  :hints (("Goal" :use (:instance big-helper-2 (lhs 0) (rhs (* x (/ y))) (c y)))))

even-is-not-oddencapsulate

(encapsulate nil
  (local (defthm even-is-not-odd-helper
      (implies (and (integerp x) (integerp y))
        (hide (not (equal (* 2 x) (+ 1 (* 2 y))))))
      :hints (("Goal" :use ((:instance (:theorem (implies (and (evenp x) (not (evenp y))) (not (equal x y))))
            (x (* 2 x))
            (y (+ 1 (* 2 y)))))) ("Subgoal 2'" :expand ((hide (not (equal (* 2 x) (+ 1 (* 2 y))))))))))
  (defthm even-is-not-odd
    (implies (and (integerp x) (integerp y))
      (not (equal (* 2 x) (+ 1 (* 2 y)))))
    :hints (("Goal" :use even-is-not-odd-helper
       :expand ((hide (not (equal (* 2 x) (+ 1 (* 2 y))))))))))