ext-compat

(encapsulate nil
  (local (include-book "arithmetic/top-with-meta" :dir :system))
  (defthm /-inverts-order-1
    (implies (and (< 0 x) (< x y) (real/rationalp x) (real/rationalp y))
      (< (/ y) (/ x))))
  (defthm /-inverts-order-2
    (implies (and (< y 0) (< x y) (real/rationalp x) (real/rationalp y))
      (< (/ y) (/ x))))
  (defthm /-inverts-weak-order
    (implies (and (< 0 x) (<= x y) (real/rationalp x) (real/rationalp y))
      (not (< (/ x) (/ y)))))
  (defthm equal-*-x-y-x
    (equal (equal (* x y) x)
      (or (equal x 0) (and (equal y 1) (acl2-numberp x)))))
  (defthm equal-*-x-y-y
    (equal (equal (* x y) y)
      (or (equal y 0) (and (equal x 1) (acl2-numberp y)))))
  (defthm equal-/
    (implies (and (acl2-numberp x) (not (equal 0 x)))
      (equal (equal (/ x) y) (equal 1 (* x y)))))
  (defthm mod-cancel-special-1-ext
    (implies (if (acl2-numberp x)
        (if (rationalp k)
          (if (acl2-numberp y)
            (if (not (equal y '0))
              (not (equal k '0))
              'nil)
            'nil)
          'nil)
        'nil)
      (equal (mod (binary-* k x) (binary-* k y))
        (binary-* k (mod x y))))))

(encapsulate nil
  (local (include-book "ihs/ihs-definitions" :dir :system))
  (local (include-book "ihs/ihs-lemmas" :dir :system))
  (local (minimal-ihs-theory))
  (defthm integerp-i/j-integerp-forward
    (implies (and (integerp (/ i j))
        (real/rationalp i)
        (integerp j)
        (not (zerop j)))
      (integerp i))
    :rule-classes ((:forward-chaining :corollary (implies (and (integerp (/ i j))
           (force (real/rationalp i))
           (integerp j)
           (force (not (equal 0 j))))
         (integerp i))) (:forward-chaining :corollary (implies (and (integerp (* (/ j) i))
            (force (real/rationalp i))
            (integerp j)
            (force (not (equal 0 j))))
          (integerp i)))))
  (defthm justify-floor-recursion-ext
    (implies (and (force (real/rationalp x))
        (force (real/rationalp y))
        (force (not (equal 0 y))))
      (and (implies (and (< 0 x) (< 1 y)) (< (floor x y) x))
        (implies (and (< x -1) (<= 2 y)) (< x (floor x y))))))
  (defthm mod-x-y-=-x-+-y-ext
    (implies (and (rationalp x)
        (rationalp y)
        (not (equal y 0))
        (if (< 0 y)
          (and (< x 0) (<= (- x) y))
          (and (< 0 x) (<= y (- x)))))
      (equal (mod x y) (+ x y)))
    :rule-classes ((:rewrite :backchain-limit-lst 0) (:rewrite :corollary (implies (and (rationalp x) (rationalp y) (not (equal y 0)))
          (equal (equal (mod x y) (+ x y))
            (if (< 0 y)
              (and (< x 0) (<= (- x) y))
              (and (< 0 x) (<= y (- x)))))))))
  (defthm mod-x-i*j
    (implies (and (> i 0)
        (> j 0)
        (force (integerp i))
        (force (integerp j))
        (force (real/rationalp x)))
      (equal (mod x (* i j))
        (+ (mod x i) (* i (mod (floor x i) j))))))
  (defthm floor-x+i*k-i*j
    (implies (and (force (real/rationalp x))
        (force (rationalp i))
        (force (integerp j))
        (force (integerp k))
        (< 0 i)
        (< 0 j)
        (<= 0 x)
        (< x i))
      (equal (floor (+ x (* i k)) (* i j)) (floor k j))))
  (defthm mod-x+i*k-i*j
    (implies (and (force (real/rationalp x))
        (force (rationalp i))
        (force (integerp j))
        (force (integerp k))
        (< 0 i)
        (< 0 j)
        (<= 0 x)
        (< x i))
      (equal (mod (+ x (* i k)) (* i j)) (+ x (* i (mod k j)))))))

(encapsulate nil
  (local (include-book "arithmetic-3/bind-free/top" :dir :system))
  (local (in-theory (enable expt)))
  (defthm expt-1-linear-b
    (implies (and (<= 0 x)
        (< x 1)
        (< 0 i)
        (real/rationalp x)
        (integerp i))
      (< (expt x i) 1))
    :rule-classes :linear :hints (("Goal" :nonlinearp t)))
  (defthm expt-1-linear-d
    (implies (and (<= 0 x)
        (<= x 1)
        (<= 0 i)
        (real/rationalp x)
        (integerp i))
      (<= (expt x i) 1))
    :rule-classes :linear :hints (("Goal" :nonlinearp t)))
  (defthm expt-1-linear-h
    (implies (and (< 0 x)
        (<= x 1)
        (< i 0)
        (real/rationalp x)
        (integerp i))
      (<= 1 (expt x i)))
    :rule-classes :linear :hints (("Goal" :nonlinearp t)))
  (local (defthm nintegerp-expt-helper
      (implies (and (< 1 x) (real/rationalp x) (< n 0) (integerp n))
        (and (< 0 (expt x n)) (< (expt x n) 1)))
      :rule-classes nil
      :hints (("Goal" :nonlinearp t))))
  (defthm nintegerp-expt
    (implies (and (real/rationalp x) (< 1 x) (integerp n) (< n 0))
      (not (integerp (expt x n))))
    :hints (("Goal" :use nintegerp-expt-helper))
    :rule-classes :type-prescription))