Theory integer

⊢ ∀i j. ediv i j = if 0 < j then i / j else -(i / -j)

⊢ ∀i j. emod i j = i % ABS j

⊢ ∀n. ABS n = if n < 0 then -n else n

⊢ ∀p q. p int_divides q ⇔ ∃m. m * p = q

⊢ ∀x y. int_max x y = if x < y then y else x

⊢ ∀x y. int_min x y = if x < y then x else y

⊢ ∀P. $LEAST_INT P = @i. P i ∧ ∀j. j < i ⇒ ¬P j

⊢ ∀i. Num i = @n. if 0 ≤ i then i = &n else i = -&n

⊢ int_0 = int_ABS tint_0

⊢ int_1 = int_ABS tint_1

⊢ ∀r. int_ABS r = int_ABS_CLASS ($tint_eq r)

⊢ ∀a. int_REP a = $@ (int_REP_CLASS a)

⊢ ∃rep. TYPE_DEFINITION (λc. ∃r. r tint_eq r ∧ c = $tint_eq r) rep

⊢ ∀T1 T2. T1 + T2 = int_ABS (int_REP T1 tint_add int_REP T2)

⊢ (∀a. int_ABS_CLASS (int_REP_CLASS a) = a) ∧
  ∀r. (λc. ∃r. r tint_eq r ∧ c = $tint_eq r) r ⇔
      int_REP_CLASS (int_ABS_CLASS r) = r

⊢ ∀i j.
    j ≠ 0 ⇒
    i / j =
    if 0 < j then
      if 0 ≤ i then &(Num i DIV Num j)
      else
        -&(Num (-i) DIV Num j) + if Num (-i) MOD Num j = 0 then 0 else -1
    else if 0 ≤ i then
      -&(Num i DIV Num (-j)) + if Num i MOD Num (-j) = 0 then 0 else -1
    else &(Num (-i) DIV Num (-j))

⊢ (∀p. p ** 0 = 1) ∧ ∀p n. p ** SUC n = p * p ** n

⊢ ∀x y. x ≥ y ⇔ y ≤ x

⊢ ∀x y. x > y ⇔ y < x

⊢ ∀x y. x ≤ y ⇔ ¬(y < x)

⊢ ∀T1 T2. T1 < T2 ⇔ int_REP T1 tint_lt int_REP T2

⊢ ∀i j. j ≠ 0 ⇒ i % j = i − i / j * j

⊢ ∀T1 T2. T1 * T2 = int_ABS (int_REP T1 tint_mul int_REP T2)

⊢ ∀T1. -T1 = int_ABS (tint_neg (int_REP T1))

⊢ ∀T1. &T1 = int_ABS (tint_of_num T1)

⊢ ∀i j.
    j ≠ 0 ⇒
    i quot j =
    if 0 < j then
      if 0 ≤ i then &(Num i DIV Num j) else -&(Num (-i) DIV Num j)
    else if 0 ≤ i then -&(Num i DIV Num (-j))
    else &(Num (-i) DIV Num (-j))

⊢ ∀i j. j ≠ 0 ⇒ i rem j = i − i quot j * j

⊢ ∀x y. x − y = x + -y

⊢ tint_0 = (1,1)

⊢ tint_1 = (1 + 1,1)

⊢ ∀x1 y1 x2 y2. (x1,y1) tint_add (x2,y2) = (x1 + x2,y1 + y2)

⊢ ∀x1 y1 x2 y2. (x1,y1) tint_eq (x2,y2) ⇔ x1 + y2 = x2 + y1

⊢ ∀x1 y1 x2 y2. (x1,y1) tint_lt (x2,y2) ⇔ x1 + y2 < x2 + y1

⊢ ∀x1 y1 x2 y2.
    (x1,y1) tint_mul (x2,y2) = (x1 * x2 + y1 * y2,x1 * y2 + y1 * x2)

⊢ ∀x y. tint_neg (x,y) = (y,x)

⊢ tint_of_num 0 = tint_0 ∧
  ∀n. tint_of_num (SUC n) = tint_of_num n tint_add tint_1

⊢ ∀x y. x = x + y ⇔ y = 0

⊢ ∀x y z. x + y = x + z ⇔ y = z

⊢ ∀P. (∀x. P x) ⇔ (∀n. P (&n)) ∧ ∀n. P (-&n)

⊢ INFINITE 𝕌(:int)

⊢ ∀n. &SUC n = &n + 1

⊢ int_0 = 0

⊢ int_1 = 1

⊢ int_1 ≠ int_0

⊢ 0 < ABS p ⇔ p ≠ 0

⊢ ∀p. ABS (ABS p) = ABS p

⊢ ∀p q.
    (ABS p = q ⇔ p = q ∧ 0 < q ∨ p = -q ∧ 0 ≤ q) ∧
    (q = ABS p ⇔ p = q ∧ 0 < q ∨ p = -q ∧ 0 ≤ q)

⊢ ∀p. ABS p = 0 ⇔ p = 0

⊢ ABS x = ABS y ⇔ x = y ∨ x = -y

⊢ ∀p. ABS p = p ⇔ 0 ≤ p

⊢ ∀p q.
    (ABS p ≤ q ⇔ p ≤ q ∧ -q ≤ p) ∧ (q ≤ ABS p ⇔ q ≤ p ∨ p ≤ -q) ∧
    (-ABS p ≤ q ⇔ -q ≤ p ∨ p ≤ q) ∧ (q ≤ -ABS p ⇔ p ≤ -q ∧ q ≤ p)

⊢ ∀p. ABS p ≤ 0 ⇔ p = 0

⊢ ∀p q.
    (ABS p < q ⇔ p < q ∧ -q < p) ∧ (q < ABS p ⇔ q < p ∨ p < -q) ∧
    (-ABS p < q ⇔ -q < p ∨ p < q) ∧ (q < -ABS p ⇔ p < -q ∧ q < p)

⊢ ∀p. ¬(ABS p < 0)

⊢ ∀p q. ABS p * ABS q = ABS (p * q)

⊢ ∀p. ABS (-p) = ABS p

⊢ ∀n. ABS (&n) = &n

⊢ ∀p. 0 ≤ ABS p

⊢ ∀p q. q ≠ 0 ⇒ ABS (p quot q * q) ≤ ABS p

⊢ ABS (i − j) = ABS (j − i)

⊢ ABS (i + j) ≤ ABS i + ABS j

⊢ ∀m n. &m + &n = &(m + n)

⊢ ∀a b c d. a + b − (c + d) = a − c + (b − d)

⊢ ∀z y x. x + (y + z) = x + y + z

⊢ ∀p n m.
    0 + p = p ∧ p + 0 = p ∧ &n + &m = &(n + m) ∧
    &n + -&m = (if m ≤ n then &(n − m) else -&(m − n)) ∧
    -&n + &m = (if n ≤ m then &(m − n) else -&(n − m)) ∧
    -&n + -&m = -&(n + m)

⊢ ∀y x. x + y = y + x

⊢ ∀i j k. k ≠ 0 ∧ (i % k = 0 ∨ j % k = 0) ⇒ (i + j) / k = i / k + j / k

⊢ ∀x. 0 + x = x

⊢ ∀x y. x + y = y ⇔ x = 0

⊢ ∀x. -x + x = 0

⊢ ∀p n m.
    0 + p = p ∧ p + 0 = p ∧ -0 = 0 ∧ --p = p ∧
    &NUMERAL n + &NUMERAL m = &NUMERAL (numeral$iZ (n + m)) ∧
    &NUMERAL n + -&NUMERAL m =
    (if m ≤ n then &NUMERAL (n − m) else -&NUMERAL (m − n)) ∧
    -&NUMERAL n + &NUMERAL m =
    (if n ≤ m then &NUMERAL (m − n) else -&NUMERAL (n − m)) ∧
    -&NUMERAL n + -&NUMERAL m = -&NUMERAL (numeral$iZ (n + m))

⊢ ∀x. x + 0 = x

⊢ ∀x y. x + y = x ⇔ y = 0

⊢ ∀x. x + -x = 0

⊢ ∀x y. x + y − x = y

⊢ ∀x y. x − (x + y) = -y

⊢ ∀y x. x + y = y + x

⊢ ∀x y. (x + y) * (x − y) = x * x − y * y

⊢ ∀x y. ¬(x < y ∧ y < x + 1)

⊢ ∀n m. m ≠ 0 ⇒ &n / &m = &(n DIV m)

⊢ (∀x. x int_divides 0) ∧ ∀x. 0 int_divides x ⇔ x = 0

⊢ ∀x. 1 int_divides x ∧ (x int_divides 1 ⇔ x = 1 ∨ x = -1)

⊢ ∀p q r. p int_divides q ⇒ (p int_divides q + r ⇔ p int_divides r)

⊢ ∀p q r. p int_divides q ⇒ p int_divides q * r

⊢ ∀p q r. p int_divides q ⇒ (p int_divides q − r ⇔ p int_divides r)

⊢ ∀p q. p int_divides q ⇔ q % p = 0 ∧ p ≠ 0 ∨ p = 0 ∧ q = 0

⊢ ∀p q. p int_divides p * q ∧ p int_divides q * p

⊢ ∀p q r. p ≠ 0 ⇒ (p * q int_divides p * r ⇔ q int_divides r)

⊢ ∀p q.
    (p int_divides -q ⇔ p int_divides q) ∧
    (-p int_divides q ⇔ p int_divides q)

⊢ ∀p q r. p int_divides q ⇒ (p int_divides r + q ⇔ p int_divides r)

⊢ ∀n m p.
    (0 int_divides 0 ⇔ T) ∧ (0 int_divides &NUMERAL (BIT1 n) ⇔ F) ∧
    (0 int_divides &NUMERAL (BIT2 n) ⇔ F) ∧ (p int_divides 0 ⇔ T) ∧
    (&NUMERAL (BIT1 n) int_divides &NUMERAL m ⇔
     NUMERAL m MOD NUMERAL (BIT1 n) = 0) ∧
    (&NUMERAL (BIT2 n) int_divides &NUMERAL m ⇔
     NUMERAL m MOD NUMERAL (BIT2 n) = 0) ∧
    (&NUMERAL (BIT1 n) int_divides -&NUMERAL m ⇔
     NUMERAL m MOD NUMERAL (BIT1 n) = 0) ∧
    (&NUMERAL (BIT2 n) int_divides -&NUMERAL m ⇔
     NUMERAL m MOD NUMERAL (BIT2 n) = 0) ∧
    (-&NUMERAL (BIT1 n) int_divides &NUMERAL m ⇔
     NUMERAL m MOD NUMERAL (BIT1 n) = 0) ∧
    (-&NUMERAL (BIT2 n) int_divides &NUMERAL m ⇔
     NUMERAL m MOD NUMERAL (BIT2 n) = 0) ∧
    (-&NUMERAL (BIT1 n) int_divides -&NUMERAL m ⇔
     NUMERAL m MOD NUMERAL (BIT1 n) = 0) ∧
    (-&NUMERAL (BIT2 n) int_divides -&NUMERAL m ⇔
     NUMERAL m MOD NUMERAL (BIT2 n) = 0)

⊢ ∀x. x int_divides x

⊢ ∀p q r. p int_divides q ⇒ p int_divides r * q

⊢ ∀p q r. p int_divides q ⇒ (p int_divides r − q ⇔ p int_divides r)

⊢ ∀x y z. x int_divides y ∧ y int_divides z ⇒ x int_divides z

⊢ ∀q. q ≠ 0 ⇒
      ∀p. p = p / q * q + p % q ∧
          if q < 0 then q < p % q ∧ p % q ≤ 0 else 0 ≤ p % q ∧ p % q < q

⊢ ∀q. q ≠ 0 ⇒ 0 / q = 0

⊢ ∀p. p / 1 = p

⊢ (∀n m. m ≠ 0 ⇒ &n / &m = &(n DIV m)) ∧ (∀p q. q ≠ 0 ⇒ p / -q = -p / q) ∧
  (∀m n. &m = &n ⇔ m = n) ∧ (∀x. -x = 0 ⇔ x = 0) ∧ ∀x. --x = x

⊢ ∀i j. j ≠ 0 ⇒ i / j = if 0 < j then ediv i j else -ediv (-i) j

⊢ ∀P x c.
    c ≠ 0 ⇒
    (P (x / c) ⇔
     ∀k r.
       x = k * c + r ∧ (c < 0 ∧ c < r ∧ r ≤ 0 ∨ ¬(c < 0) ∧ 0 ≤ r ∧ r < c) ⇒
       P k)

⊢ ∀p. p ≠ 0 ⇒ p / p = 1

⊢ ∀i j. i ≠ 0 ⇒ i * j / i = j

⊢ ∀p q. q ≠ 0 ∧ p % q = 0 ⇒ p / q * q = p

⊢ ∀p q. q ≠ 0 ⇒ p / -q = -p / q

⊢ ∀P x c.
    c ≠ 0 ⇒
    (P (x / c) ⇔
     ∃k r.
       x = k * c + r ∧ (c < 0 ∧ c < r ∧ r ≤ 0 ∨ ¬(c < 0) ∧ 0 ≤ r ∧ r < c) ∧
       P k)

⊢ ∀m n.
    0 / &NUMERAL (BIT1 n) = 0 ∧ 0 / &NUMERAL (BIT2 n) = 0 ∧
    &NUMERAL m / &NUMERAL (BIT1 n) = &(NUMERAL m DIV NUMERAL (BIT1 n)) ∧
    &NUMERAL m / &NUMERAL (BIT2 n) = &(NUMERAL m DIV NUMERAL (BIT2 n)) ∧
    -&NUMERAL m / &NUMERAL (BIT1 n) =
    -&(NUMERAL m DIV NUMERAL (BIT1 n)) +
    (if NUMERAL m MOD NUMERAL (BIT1 n) = 0 then 0 else -1) ∧
    -&NUMERAL m / &NUMERAL (BIT2 n) =
    -&(NUMERAL m DIV NUMERAL (BIT2 n)) +
    (if NUMERAL m MOD NUMERAL (BIT2 n) = 0 then 0 else -1) ∧
    &NUMERAL m / -&NUMERAL (BIT1 n) =
    -&(NUMERAL m DIV NUMERAL (BIT1 n)) +
    (if NUMERAL m MOD NUMERAL (BIT1 n) = 0 then 0 else -1) ∧
    &NUMERAL m / -&NUMERAL (BIT2 n) =
    -&(NUMERAL m DIV NUMERAL (BIT2 n)) +
    (if NUMERAL m MOD NUMERAL (BIT2 n) = 0 then 0 else -1) ∧
    -&NUMERAL m / -&NUMERAL (BIT1 n) = &(NUMERAL m DIV NUMERAL (BIT1 n)) ∧
    -&NUMERAL m / -&NUMERAL (BIT2 n) = &(NUMERAL m DIV NUMERAL (BIT2 n))

⊢ ∀i j. i ≠ 0 ⇒ j * i / i = j

⊢ ∀i j q.
    (∃r. i = q * j + r ∧ if j < 0 then j < r ∧ r ≤ 0 else 0 ≤ r ∧ r < j) ⇒
    i / j = q

⊢ ∀x. x + x = 2 * x

⊢ ∀x y. x * y = 0 ⇔ x = 0 ∨ y = 0

⊢ (∀m n. &m = &n ⇔ m = n) ∧ (∀x y. -x = -y ⇔ x = y) ∧
  ∀n m. (&n = -&m ⇔ n = 0 ∧ m = 0) ∧ (-&n = &m ⇔ n = 0 ∧ m = 0)

⊢ ∀x y. x = y ⇒ x ≤ y

⊢ ∀x y z. x + y = x + z ⇔ y = z

⊢ ∀x y z. x * y = x * z ⇔ x = 0 ∨ y = z

⊢ ∀x y z. x ≠ 0 ⇒ (y = z ⇔ x * y = x * z)

⊢ ∀x y z. x ≠ 0 ∧ x * y = x * z ⇒ y = z

⊢ ∀x y. -x = -y ⇔ x = y

⊢ ∀x y z. x + z = y + z ⇔ x = y

⊢ ∀n m.
    (0 = 0 ⇔ T) ∧ (0 = &NUMERAL (BIT1 n) ⇔ F) ∧
    (0 = &NUMERAL (BIT2 n) ⇔ F) ∧ (0 = -&NUMERAL (BIT1 n) ⇔ F) ∧
    (0 = -&NUMERAL (BIT2 n) ⇔ F) ∧ (&NUMERAL (BIT1 n) = 0 ⇔ F) ∧
    (&NUMERAL (BIT2 n) = 0 ⇔ F) ∧ (-&NUMERAL (BIT1 n) = 0 ⇔ F) ∧
    (-&NUMERAL (BIT2 n) = 0 ⇔ F) ∧ (&NUMERAL n = &NUMERAL m ⇔ n = m) ∧
    (&NUMERAL (BIT1 n) = -&NUMERAL m ⇔ F) ∧
    (&NUMERAL (BIT2 n) = -&NUMERAL m ⇔ F) ∧
    (-&NUMERAL (BIT1 n) = &NUMERAL m ⇔ F) ∧
    (-&NUMERAL (BIT2 n) = &NUMERAL m ⇔ F) ∧
    (-&NUMERAL n = -&NUMERAL m ⇔ n = m)

⊢ ∀x y z. x * z = y * z ⇔ z = 0 ∨ x = y

⊢ ∀x y z. z ≠ 0 ∧ x * z = y * z ⇒ x = y

⊢ ∀x y z. x = y − z ⇔ x + z = y

⊢ ∀x y z. x − y = z ⇔ x = z + y

⊢ ∀n m. &n ** m = &(n ** m)

⊢ ∀n m p. p ** n * p ** m = p ** (n + m)

⊢ ∀p n m.
    p ** 0 = 1 ∧ &n ** m = &(n ** m) ∧
    -&n ** NUMERAL (BIT1 m) = -&NUMERAL (n ** NUMERAL (BIT1 m)) ∧
    -&n ** NUMERAL (BIT2 m) = &NUMERAL (n ** NUMERAL (BIT2 m))

⊢ ∀p n. p ** n = 0 ⇔ p = 0 ∧ n ≠ 0

⊢ ∀m n p. n ≤ m ∧ p ≠ 0 ⇒ p ** m % p ** n = 0

⊢ ∀m n p. (p ** n) ** m = p ** (n * m)

⊢ ∀n m. (EVEN n ⇒ -&m ** n = &(m ** n)) ∧ (ODD n ⇒ -&m ** n = -&(m ** n))

⊢ ∀n m p.
    p ** 0 = 1 ∧ &NUMERAL n ** NUMERAL m = &NUMERAL (n ** m) ∧
    -&NUMERAL n ** NUMERAL (BIT1 m) = -&NUMERAL (n ** BIT1 m) ∧
    -&NUMERAL n ** NUMERAL (BIT2 m) = &NUMERAL (n ** BIT2 m)

⊢ ∀m n p. n ≤ m ∧ p ≠ 0 ⇒ p ** m / p ** n = p ** (m − n)

⊢ ∀x y. x ≥ y ⇔ y ≤ x

⊢ ∀x y. x ≥ y ⇔ y ≤ x

⊢ ∀n m.
    (0 ≥ 0 ⇔ T) ∧ (&NUMERAL n ≥ 0 ⇔ T) ∧ (-&NUMERAL (BIT1 n) ≥ 0 ⇔ F) ∧
    (-&NUMERAL (BIT2 n) ≥ 0 ⇔ F) ∧ (0 ≥ &NUMERAL (BIT1 n) ⇔ F) ∧
    (0 ≥ &NUMERAL (BIT2 n) ⇔ F) ∧ (0 ≥ -&NUMERAL (BIT1 n) ⇔ T) ∧
    (0 ≥ -&NUMERAL (BIT2 n) ⇔ T) ∧ (&NUMERAL m ≥ &NUMERAL n ⇔ n ≤ m) ∧
    (-&NUMERAL (BIT1 m) ≥ &NUMERAL n ⇔ F) ∧
    (-&NUMERAL (BIT2 m) ≥ &NUMERAL n ⇔ F) ∧
    (&NUMERAL m ≥ -&NUMERAL n ⇔ T) ∧ (-&NUMERAL m ≥ -&NUMERAL n ⇔ m ≤ n)

⊢ ∀x y. x > y ⇔ y < x

⊢ ∀x y. x > y ⇔ y < x

⊢ ∀n m.
    (&NUMERAL (BIT1 n) > 0 ⇔ T) ∧ (&NUMERAL (BIT2 n) > 0 ⇔ T) ∧
    (0 > 0 ⇔ F) ∧ (-&NUMERAL n > 0 ⇔ F) ∧ (0 > &NUMERAL n ⇔ F) ∧
    (0 > -&NUMERAL (BIT1 n) ⇔ T) ∧ (0 > -&NUMERAL (BIT2 n) ⇔ T) ∧
    (&NUMERAL m > &NUMERAL n ⇔ n < m) ∧
    (&NUMERAL m > -&NUMERAL (BIT1 n) ⇔ T) ∧
    (&NUMERAL m > -&NUMERAL (BIT2 n) ⇔ T) ∧
    (-&NUMERAL m > &NUMERAL n ⇔ F) ∧ (-&NUMERAL m > -&NUMERAL n ⇔ m < n)

⊢ ∀m n. &m = &n ⇔ m = n

⊢ (∀x. 0 * x = 0) ∧ (∀x y z. x + y = x + z ⇔ y = z) ∧
  ∀w x y z. w * y + x * z = w * z + x * y ⇔ w = x ∨ y = z

⊢ ∀z y x. x * (y + z) = x * y + x * z

⊢ ∀m n. &m ≤ &n ⇔ m ≤ n

⊢ ∀i j. 0 ≤ i ∧ i < j ⇒ i % j = i

⊢ ∀x y. 0 ≤ x ∧ 0 < y ⇒ 0 < x + y

⊢ ∀w x y z. w ≤ x ∧ y < z ⇒ w + y < x + z

⊢ ∀x y. ¬(x < y ∧ y ≤ x)

⊢ ∀x y. x ≤ y ∨ y < x

⊢ ∀x y z. x ≤ y ∧ y < z ⇒ x < z

⊢ 0 ≤ 1

⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x + y

⊢ ∀w x y z. w ≤ x ∧ y ≤ z ⇒ w + y ≤ x + z

⊢ ∀x y. y ≤ x + y ⇔ 0 ≤ x

⊢ ∀x y. x ≤ x + y ⇔ 0 ≤ y

⊢ ∀x y. x ≤ y ∧ y ≤ x ⇔ x = y

⊢ ∀x y. x ≤ y ⇔ x < y ∨ x = y

⊢ ∀x. 0 ≤ x + x ⇔ 0 ≤ x

⊢ ∀x y z. x + y ≤ x + z ⇔ y ≤ z

⊢ ∀x y. -x ≤ y ⇔ 0 ≤ x + y

⊢ ∀x y. x ≤ y ⇔ x < y ∨ x = y

⊢ x ≤ y ⇔ x < y + 1

⊢ ∀x y z. 0 < x ⇒ (x * y ≤ x * z ⇔ y ≤ z)

⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x * y

⊢ ∀x y. -x ≤ -y ⇔ y ≤ x

⊢ ∀x. -x ≤ x ⇔ 0 ≤ x

⊢ ∀x. x ≤ -x ⇔ x ≤ 0

⊢ ∀x. 0 ≤ x ∨ 0 ≤ -x

⊢ ∀x y z. x + z ≤ y + z ⇔ x ≤ y

⊢ ∀n m.
    (0 ≤ 0 ⇔ T) ∧ (0 ≤ &NUMERAL n ⇔ T) ∧ (0 ≤ -&NUMERAL (BIT1 n) ⇔ F) ∧
    (0 ≤ -&NUMERAL (BIT2 n) ⇔ F) ∧ (&NUMERAL (BIT1 n) ≤ 0 ⇔ F) ∧
    (&NUMERAL (BIT2 n) ≤ 0 ⇔ F) ∧ (-&NUMERAL (BIT1 n) ≤ 0 ⇔ T) ∧
    (-&NUMERAL (BIT2 n) ≤ 0 ⇔ T) ∧ (&NUMERAL n ≤ &NUMERAL m ⇔ n ≤ m) ∧
    (&NUMERAL n ≤ -&NUMERAL (BIT1 m) ⇔ F) ∧
    (&NUMERAL n ≤ -&NUMERAL (BIT2 m) ⇔ F) ∧
    (-&NUMERAL n ≤ &NUMERAL m ⇔ T) ∧ (-&NUMERAL n ≤ -&NUMERAL m ⇔ m ≤ n)

⊢ ∀x. x ≤ x

⊢ ∀x y. x ≤ -y ⇔ x + y ≤ 0

⊢ ∀x. 0 ≤ x * x

⊢ ∀x y z. x ≤ y − z ⇔ x + z ≤ y

⊢ ∀x y z. x − y ≤ z ⇔ x ≤ z + y

⊢ ∀x y. x ≤ y ∨ y ≤ x

⊢ ∀x y z. x ≤ y ∧ y ≤ z ⇒ x ≤ z

⊢ ∀x y. x + y = 0 ⇔ x = -y

⊢ ∀m n. &m < &n ⇔ m < n

⊢ ∀x y. x < y ⇔ ¬(y ≤ x)

⊢ ∀x y. 0 < x ∧ 0 ≤ y ⇒ 0 < x + y

⊢ ∀w x y z. w < x ∧ y ≤ z ⇒ w + y < x + z

⊢ ∀x y. ¬(x ≤ y ∧ y < x)

⊢ ∀x y. x < y ∨ y ≤ x

⊢ ∀x y z. x < y ∧ y ≤ z ⇒ x < z

⊢ 0 < 1

⊢ ∀x y. 0 < x ∧ 0 < y ⇒ 0 < x + y

⊢ ∀x y. x ≤ y ⇒ x < y + 1

⊢ ∀w x y z. w < x ∧ y < z ⇒ w + y < x + z

⊢ ∀x y. y < x + y ⇔ 0 < x

⊢ ∀x y z. y < x + -z ⇔ y + z < x

⊢ ∀x y z. x + -y < z ⇔ x < z + y

⊢ ∀x y. x < x + y ⇔ 0 < y

⊢ ∀x y z. x + y < z ⇔ x < z − y

⊢ ∀x y. ¬(x < y ∧ y < x)

⊢ ∀n m.
    (&n < &m ⇔ n < m) ∧ (-&n < -&m ⇔ m < n) ∧ (-&n < &m ⇔ n ≠ 0 ∨ m ≠ 0) ∧
    (&n < -&m ⇔ F)

⊢ ∀x y. x < y ⇔ x + 1 ≤ y

⊢ ∀x y. x < y ⇒ ¬(y < x)

⊢ ∀x y. x < y ⇒ x ≤ y

⊢ ∀x y. x < y ⇒ x ≠ y

⊢ ∀x y z. x + y < x + z ⇔ y < z

⊢ ∀x y z. y < z ⇒ x + y < x + z

⊢ ∀x y. x < y ⇔ x ≤ y ∧ x ≠ y

⊢ x < y ⇔ x + 1 ≤ y

⊢ ∀x y z. 0 < x ⇒ (x * y < x * z ⇔ y < z)

⊢ ∀x y. int_0 < x ∧ int_0 < y ⇒ int_0 < x * y

⊢ ∀x1 x2 y1 y2. 0 ≤ x1 ∧ 0 ≤ y1 ∧ x1 < x2 ∧ y1 < y2 ⇒ x1 * y1 < x2 * y2

⊢ ∀x y. -x < -y ⇔ y < x

⊢ ∀x. x = 0 ∨ 0 < x ∨ 0 < -x

⊢ ∀n. &n ≠ 0 ⇔ 0 < &n

⊢ ∀x y z. x + z < y + z ⇔ x < y

⊢ ∀n m.
    (0 < &NUMERAL (BIT1 n) ⇔ T) ∧ (0 < &NUMERAL (BIT2 n) ⇔ T) ∧
    (0 < 0 ⇔ F) ∧ (0 < -&NUMERAL n ⇔ F) ∧ (&NUMERAL n < 0 ⇔ F) ∧
    (-&NUMERAL (BIT1 n) < 0 ⇔ T) ∧ (-&NUMERAL (BIT2 n) < 0 ⇔ T) ∧
    (&NUMERAL n < &NUMERAL m ⇔ n < m) ∧
    (-&NUMERAL (BIT1 n) < &NUMERAL m ⇔ T) ∧
    (-&NUMERAL (BIT2 n) < &NUMERAL m ⇔ T) ∧
    (&NUMERAL n < -&NUMERAL m ⇔ F) ∧ (-&NUMERAL n < -&NUMERAL m ⇔ m < n)

⊢ ∀x. ¬(x < x)

⊢ ∀x y z. x < y − z ⇔ x + z < y

⊢ ∀x y z. x − y < z ⇔ x < z + y

⊢ ∀x y. x = y ∨ x < y ∨ y < x

⊢ ∀x y z. x < y ∧ y < z ⇒ x < z

⊢ ∀x y z. int_max x y < z ⇒ x < z ∧ y < z

⊢ ∀m n. int_max (&m) (&n) = &MAX m n

⊢ ∀x y z. x < int_min y z ⇒ x < y ∧ x < z

⊢ ∀m n. int_min (&m) (&n) = &MIN m n

⊢ ∀n m. m ≠ 0 ⇒ &n % &m = &(n MOD m)

⊢ ∀p. p ≠ 0 ⇒ 0 % p = 0

⊢ ∀i. i % 1 = 0

⊢ k ≠ 0 ⇒ (q * k + r) % k = r % k

⊢ ∀p q.
    q ≠ 0 ⇒ if q < 0 then q < p % q ∧ p % q ≤ 0 else 0 ≤ p % q ∧ p % q < q

⊢ (∀n m. m ≠ 0 ⇒ &n % &m = &(n MOD m)) ∧
  (∀p q. q ≠ 0 ⇒ p % -q = -(-p % q)) ∧ (∀x. --x = x) ∧
  (∀m n. &m = &n ⇔ m = n) ∧ ∀x. -x = 0 ⇔ x = 0

⊢ ∀p. p ≠ 0 ⇒ ∀q. (q * p) % p = 0

⊢ ∀i j. j ≠ 0 ⇒ i % j = if 0 < j then emod i j else -emod (-i) j

⊢ ∀q. q ≠ 0 ⇒ ∀p. p % q = 0 ⇔ ∃k. p = k * q

⊢ ∀P x c.
    c ≠ 0 ⇒
    (P (x % c) ⇔
     ∀q r.
       x = q * c + r ∧ (c < 0 ∧ c < r ∧ r ≤ 0 ∨ ¬(c < 0) ∧ 0 ≤ r ∧ r < c) ⇒
       P r)

⊢ ∀i. i ≠ 0 ⇒ i % i = 0

⊢ ∀n. 0 < n ⇒ -1 % n = n − 1

⊢ k ≠ 0 ⇒ j % k % k = j % k

⊢ ∀p q. q ≠ 0 ⇒ p % -q = -(-p % q)

⊢ k ≠ 0 ⇒ -x % k = (k − x) % k

⊢ ∀P x c.
    c ≠ 0 ⇒
    (P (x % c) ⇔
     ∃k r.
       x = k * c + r ∧ (c < 0 ∧ c < r ∧ r ≤ 0 ∨ ¬(c < 0) ∧ 0 ≤ r ∧ r < c) ∧
       P r)

⊢ k ≠ 0 ⇒ (i % k + j % k) % k = (i + j) % k

⊢ ∀m n.
    0 % &NUMERAL (BIT1 n) = 0 ∧ 0 % &NUMERAL (BIT2 n) = 0 ∧
    0 % -&NUMERAL (BIT1 n) = 0 ∧ 0 % -&NUMERAL (BIT2 n) = 0 ∧
    &NUMERAL m % &NUMERAL (BIT1 n) = &(NUMERAL m MOD NUMERAL (BIT1 n)) ∧
    &NUMERAL m % &NUMERAL (BIT2 n) = &(NUMERAL m MOD NUMERAL (BIT2 n)) ∧
    &NUMERAL m % -&NUMERAL (BIT1 n) = -(-&NUMERAL m % &NUMERAL (BIT1 n)) ∧
    &NUMERAL m % -&NUMERAL (BIT2 n) = -(-&NUMERAL m % &NUMERAL (BIT2 n)) ∧
    x % &NUMERAL (BIT1 n) = x − x / &NUMERAL (BIT1 n) * &NUMERAL (BIT1 n) ∧
    x % &NUMERAL (BIT2 n) = x − x / &NUMERAL (BIT2 n) * &NUMERAL (BIT2 n) ∧
    x % -&NUMERAL (BIT1 n) = -x / &NUMERAL (BIT1 n) * &NUMERAL (BIT1 n) + x ∧
    x % -&NUMERAL (BIT2 n) = -x / &NUMERAL (BIT2 n) * &NUMERAL (BIT2 n) + x

⊢ k ≠ 0 ⇒ (i % k − j % k) % k = (i − j) % k

⊢ ∀i j m.
    (∃q. i = q * j + m ∧ if j < 0 then j < m ∧ m ≤ 0 else 0 ≤ m ∧ m < j) ⇒
    i % j = m

⊢ ∀m n. &m * &n = &(m * n)

⊢ ∀z y x. x * (y * z) = x * y * z

⊢ (∀m n. &m * &n = &(m * n)) ∧ (∀x y. -x * y = -(x * y)) ∧
  (∀x y. x * -y = -(x * y)) ∧ ∀x. --x = x

⊢ ∀y x. x * y = y * x

⊢ ∀p q k. q ≠ 0 ∧ p % q = 0 ⇒ k * p / q = k * (p / q)

⊢ ∀x y. x * y = 1 ⇔ x = 1 ∧ y = 1 ∨ x = -1 ∧ y = -1

⊢ ∀x. 1 * x = x

⊢ ∀x y. -x * y = -(x * y)

⊢ ∀x. 0 * x = 0

⊢ ∀p q k. q ≠ 0 ∧ p rem q = 0 ⇒ k * p quot q = k * (p quot q)

⊢ ∀m n p.
    p * 0 = 0 ∧ 0 * p = 0 ∧ &NUMERAL m * &NUMERAL n = &NUMERAL (m * n) ∧
    -&NUMERAL m * &NUMERAL n = -&NUMERAL (m * n) ∧
    &NUMERAL m * -&NUMERAL n = -&NUMERAL (m * n) ∧
    -&NUMERAL m * -&NUMERAL n = &NUMERAL (m * n)

⊢ ∀x. x * 1 = x

⊢ ∀x y. x * -y = -(x * y)

⊢ ∀x. x * 0 = 0

⊢ ∀p q.
    (0 < p * q ⇔ 0 < p ∧ 0 < q ∨ p < 0 ∧ q < 0) ∧
    (p * q < 0 ⇔ 0 < p ∧ q < 0 ∨ p < 0 ∧ 0 < q)

⊢ ∀y x. x * y = y * x

⊢ ∀x. --x = x

⊢ -0 = 0

⊢ ∀x y. -(x + y) = -x + -y

⊢ ∀x y. -x = y ⇔ x = -y

⊢ ∀x. -x = 0 ⇔ x = 0

⊢ ∀x. 0 ≤ -x ⇔ x ≤ 0

⊢ ∀x. 0 < -x ⇔ x < 0

⊢ ∀x. -x ≤ 0 ⇔ 0 ≤ x

⊢ ∀x y. -(x * y) = -x * y

⊢ ∀x. -x < 0 ⇔ 0 < x

⊢ ∀x. -x = -1 * x

⊢ ∀x y. -x * -y = x * y

⊢ ∀x. --x = x

⊢ ∀x y. -(x * y) = x * -y

⊢ ∀p. p = -p ⇔ p = 0

⊢ ∀x y. -(x − y) = y − x

⊢ ∀x y. x ≠ y ⇔ x < y ∨ y < x

⊢ ∀x y. ¬(x ≤ y) ⇔ y < x

⊢ ∀x y. ¬(x < y) ⇔ y ≤ x

⊢ ∀p. (∃n. p = &n ∧ n ≠ 0) ∨ (∃n. p = -&n ∧ n ≠ 0) ∨ p = 0

⊢ ∀n. n ≠ 0 ⇒ 0 < &n

⊢ ∀i. &Num i = i ⇔ 0 ≤ i

⊢ ∀m n. &m + &n = &(m + n)

⊢ ∀m n. &m = &n ⇔ m = n

⊢ ∀m n. &m ≤ &n ⇔ m ≤ n

⊢ ∀m n. &m < &n ⇔ m < n

⊢ ∀m n. &m * &n = &(m * n)

⊢ ∀n m. &n ** m = &(n ** m)

⊢ (∀x. -x = -1 * x) ∧ ∀x y. x − y = x + -1 * y

⊢ 1 * x = x ∧ a * m + b * m = (a + b) * m ∧ a * m + m = (a + 1) * m ∧
  m + a * m = (a + 1) * m ∧ m + m = (1 + 1) * m ∧ 0 * m = 0 ∧ 0 + a = a ∧
  a + 0 = a ∧ a * b = b * a ∧ (a + b) * c = a * c + b * c ∧ 0 * a = 0 ∧
  a * 0 = 0 ∧ 1 * a = a ∧ a * 1 = a ∧
  lx * ly * (rx * ry) = lx * rx * (ly * ry) ∧
  lx * ly * (rx * ry) = lx * (ly * (rx * ry)) ∧
  lx * ly * (rx * ry) = rx * (lx * ly * ry) ∧ lx * ly * rx = lx * rx * ly ∧
  lx * ly * rx = lx * (ly * rx) ∧ lx * rx = rx * lx ∧
  lx * (rx * ry) = lx * rx * ry ∧ lx * (rx * ry) = rx * (lx * ry) ∧
  a + b + (c + d) = a + c + (b + d) ∧ a + b + c = a + (b + c) ∧
  a + (c + d) = c + (a + d) ∧ a + b + c = a + c + b ∧ a + c = c + a ∧
  a + (c + d) = a + c + d ∧ x ** p * x ** q = x ** (p + q) ∧
  x * x ** q = x ** SUC q ∧ x ** q * x = x ** SUC q ∧ x * x = x ** 2 ∧
  (x * y) ** q = x ** q * y ** q ∧ (x ** p) ** q = x ** (p * q) ∧
  x ** 0 = 1 ∧ x ** 1 = x ∧ x * (y + z) = x * y + x * z ∧
  x ** SUC q = x * x ** q

⊢ ∀n. 0 ≤ &n

⊢ ∀x. 0 < x * x ⇔ x ≠ 0

⊢ ∀x. 0 < x ⇒ x ≠ 0

⊢ x ** 0 = 1 ∧ ∀n. x ** SUC n = x * x ** n

⊢ ∀x n. -x ** n = if EVEN n then x ** n else -(x ** n)

⊢ ∀p q. q ≠ 0 ⇒ &p quot &q = &(p DIV q)

⊢ ∀q. q ≠ 0 ⇒ 0 quot q = 0

⊢ ∀p. p quot 1 = p

⊢ (∀p q. q ≠ 0 ⇒ &p quot &q = &(p DIV q)) ∧
  (∀p q. q ≠ 0 ⇒ -p quot q = -(p quot q) ∧ p quot -q = -(p quot q)) ∧
  (∀m n. &m = &n ⇔ m = n) ∧ (∀x. -x = 0 ⇔ x = 0) ∧ ∀x. --x = x

⊢ ∀i j. j ≠ 0 ⇒ i quot j = if 0 ≤ i then ediv i j else ediv (-i) (-j)

⊢ ∀p. p ≠ 0 ⇒ p quot p = 1

⊢ ∀p q. q ≠ 0 ⇒ -p quot q = -(p quot q) ∧ p quot -q = -(p quot q)

⊢ ∀m n.
    0 quot &NUMERAL (BIT1 n) = 0 ∧ 0 quot &NUMERAL (BIT2 n) = 0 ∧
    &NUMERAL m quot &NUMERAL (BIT1 n) = &(NUMERAL m DIV NUMERAL (BIT1 n)) ∧
    &NUMERAL m quot &NUMERAL (BIT2 n) = &(NUMERAL m DIV NUMERAL (BIT2 n)) ∧
    -&NUMERAL m quot &NUMERAL (BIT1 n) = -&(NUMERAL m DIV NUMERAL (BIT1 n)) ∧
    -&NUMERAL m quot &NUMERAL (BIT2 n) = -&(NUMERAL m DIV NUMERAL (BIT2 n)) ∧
    &NUMERAL m quot -&NUMERAL (BIT1 n) = -&(NUMERAL m DIV NUMERAL (BIT1 n)) ∧
    &NUMERAL m quot -&NUMERAL (BIT2 n) = -&(NUMERAL m DIV NUMERAL (BIT2 n)) ∧
    -&NUMERAL m quot -&NUMERAL (BIT1 n) = &(NUMERAL m DIV NUMERAL (BIT1 n)) ∧
    -&NUMERAL m quot -&NUMERAL (BIT2 n) = &(NUMERAL m DIV NUMERAL (BIT2 n))

⊢ ∀p q k.
    (∃r. p = k * q + r ∧ (if 0 < p then 0 ≤ r else r ≤ 0) ∧ ABS r < ABS q) ⇒
    p quot q = k

⊢ ∀x y z. (x + y) * z = x * z + y * z

⊢ ∀p q. q ≠ 0 ⇒ &p rem &q = &(p MOD q)

⊢ ∀q. q ≠ 0 ⇒ 0 rem q = 0

⊢ ∀q. q ≠ 0 ⇒
      ∀p. p = p quot q * q + p rem q ∧
          (if 0 < p then 0 ≤ p rem q else p rem q ≤ 0) ∧
          ABS (p rem q) < ABS q

⊢ (∀p q. q ≠ 0 ⇒ &p rem &q = &(p MOD q)) ∧
  (∀p q. q ≠ 0 ⇒ -p rem q = -(p rem q) ∧ p rem -q = p rem q) ∧
  (∀x. --x = x) ∧ (∀m n. &m = &n ⇔ m = n) ∧ ∀x. -x = 0 ⇔ x = 0

⊢ ∀p. p ≠ 0 ⇒ ∀q. (q * p) rem p = 0

⊢ ∀i j. j ≠ 0 ⇒ i rem j = if 0 ≤ i then emod i j else -emod (-i) j

⊢ ∀q. q ≠ 0 ⇒ ∀p. p rem q = 0 ⇔ ∃k. p = k * q

⊢ ∀i n. 0 < n ⇒ i rem n = if i < 0 then (i − 1) % n − n + 1 else i % n

⊢ ∀p. p ≠ 0 ⇒ p rem p = 0

⊢ ∀p q. q ≠ 0 ⇒ -p rem q = -(p rem q) ∧ p rem -q = p rem q

⊢ ∀m n.
    0 rem &NUMERAL (BIT1 n) = 0 ∧ 0 rem &NUMERAL (BIT2 n) = 0 ∧
    &NUMERAL m rem &NUMERAL (BIT1 n) = &(NUMERAL m MOD NUMERAL (BIT1 n)) ∧
    &NUMERAL m rem &NUMERAL (BIT2 n) = &(NUMERAL m MOD NUMERAL (BIT2 n)) ∧
    -&NUMERAL m rem &NUMERAL (BIT1 n) = -&(NUMERAL m MOD NUMERAL (BIT1 n)) ∧
    -&NUMERAL m rem &NUMERAL (BIT2 n) = -&(NUMERAL m MOD NUMERAL (BIT2 n)) ∧
    &NUMERAL m rem -&NUMERAL (BIT1 n) = &(NUMERAL m MOD NUMERAL (BIT1 n)) ∧
    &NUMERAL m rem -&NUMERAL (BIT2 n) = &(NUMERAL m MOD NUMERAL (BIT2 n)) ∧
    -&NUMERAL m rem -&NUMERAL (BIT1 n) = -&(NUMERAL m MOD NUMERAL (BIT1 n)) ∧
    -&NUMERAL m rem -&NUMERAL (BIT2 n) = -&(NUMERAL m MOD NUMERAL (BIT2 n))

⊢ ∀p q r.
    ABS r < ABS q ∧ (if 0 < p then 0 ≤ r else r ≤ 0) ∧ (∃k. p = k * q + r) ⇒
    p rem q = r

⊢ ∀x y. x + y = 0 ⇔ y = -x

⊢ ∀n m. m ≤ n ⇒ &n − &m = &(n − m)

⊢ ∀x y. x − y = 0 ⇔ x = y

⊢ ABS i − ABS j ≤ ABS (i − j)

⊢ ∀x y. x − y + y = x

⊢ ∀x y. y + (x − y) = x

⊢ ∀x y. x − y = x + -y

⊢ ∀x y z. x * (y − z) = x * y − x * z

⊢ ∀x y. 0 ≤ x − y ⇔ y ≤ x

⊢ ∀x y. -x − y = -(x + y)

⊢ ∀x y. 0 < x − y ⇔ y < x

⊢ ∀x. 0 − x = -x

⊢ ∀x y. -x − -y = y − x

⊢ ∀x y z. (x − y) * z = x * z − y * z

⊢ ∀m n p.
    p − 0 = p ∧ 0 − p = -p ∧
    &NUMERAL m − &NUMERAL n = &NUMERAL m + -&NUMERAL n ∧
    -&NUMERAL m − &NUMERAL n = -&NUMERAL m + -&NUMERAL n ∧
    &NUMERAL m − -&NUMERAL n = &NUMERAL m + &NUMERAL n ∧
    -&NUMERAL m − -&NUMERAL n = -&NUMERAL m + &NUMERAL n

⊢ ∀x. x − x = 0

⊢ ∀x y. x − -y = x + y

⊢ ∀x. x − 0 = x

⊢ ∀x y. x − y − x = -y

⊢ ∀x y. x − (x − y) = y

⊢ ∀a b c. a − b + (b − c) = a − c

⊢ ∀x y. x * x + y * y = 0 ⇔ x = 0 ∧ y = 0

⊢ ∀n i. &n ≤ i ⇒ n ≤ Num i

⊢ ∀x1 x2 y1 y2. x1 < y1 ∧ x2 < y2 ⇒ x1 + x2 < y1 + y2

⊢ ∀x y. x < x + y ⇔ 0 < y

⊢ ∀x y. ¬(x + y < x)

⊢ ∀x y z. x + y < x + z ⇔ y < z

⊢ Num i = 0 ⇔ i = 0

⊢ ∀m n. m + n = Num (&m + &n)

⊢ ∀n m. n DIV m = if m = 0 then 0 else Num (ediv (&n) (&m))

⊢ ∀n m. n MOD m = if m = 0 then n else Num (emod (&n) (&m))

⊢ ∀m n. m * n = Num (&m * &n)

⊢ ∀m n. m − n = if &m ≤ &n then 0 else Num (&m − &n)

⊢ 0 ≤ x ∧ 0 ≤ y ⇒ (Num x < Num y ⇔ x < y)

⊢ ∀i. i ≤ 0 ⇒ ∃n. i = -&n

⊢ ∀n. Num (&n) = n

⊢ ∀n. Num (-&n) = n

⊢ ∀i. 0 ≤ i ⇒ ∃!n. i = &n

⊢ ∀t. ¬(t < int_0) ⇒ ∃n. t = &n

⊢ ∀i. 0 ≤ i ⇒ ∃n. i = &n

⊢ ∀t. ¬(t tint_lt tint_0) ⇒ ∃n. t tint_eq tint_of_num n

⊢ Num a = Num b ⇔ a = b ∨ a = -b

⊢ ∀i. &Num i = ABS i

⊢ Num (-a) = Num a

⊢ ¬(tint_1 tint_eq tint_0)

⊢ ∀z y x. x tint_add (y tint_add z) = x tint_add y tint_add z

⊢ ∀x. tint_0 tint_add x tint_eq x

⊢ ∀x. tint_neg x tint_add x tint_eq tint_0

⊢ ∀y x. x tint_add y = y tint_add x

⊢ ∀x1 x2 y1 y2.
    x1 tint_eq x2 ∧ y1 tint_eq y2 ⇒ x1 tint_add y1 tint_eq x2 tint_add y2

⊢ ∀x1 x2 y. x1 tint_eq x2 ⇒ x1 tint_add y tint_eq x2 tint_add y

⊢ ∀p q. p = q ⇒ p tint_eq q

⊢ ∀p q. p tint_eq q ⇔ $tint_eq p = $tint_eq q

⊢ ∀x. x tint_eq x

⊢ ∀x y. x tint_eq y ⇔ y tint_eq x

⊢ ∀x y z. x tint_eq y ∧ y tint_eq z ⇒ x tint_eq z

⊢ ∀m n. tint_of_num m tint_eq tint_of_num n ⇔ m = n

⊢ ∀z y x. x tint_mul (y tint_add z) = x tint_mul y tint_add x tint_mul z

⊢ ∀x y z. y tint_lt z ⇒ x tint_add y tint_lt x tint_add z

⊢ ∀x y. tint_0 tint_lt x ∧ tint_0 tint_lt y ⇒ tint_0 tint_lt x tint_mul y

⊢ ∀x. ¬(x tint_lt x)

⊢ ∀x y. x tint_eq y ∨ x tint_lt y ∨ y tint_lt x

⊢ ∀x y z. x tint_lt y ∧ y tint_lt z ⇒ x tint_lt z

⊢ ∀x1 x2 y1 y2.
    x1 tint_eq x2 ∧ y1 tint_eq y2 ⇒ (x1 tint_lt y1 ⇔ x2 tint_lt y2)

⊢ ∀x y1 y2. y1 tint_eq y2 ⇒ (x tint_lt y1 ⇔ x tint_lt y2)

⊢ ∀x1 x2 y. x1 tint_eq x2 ⇒ (x1 tint_lt y ⇔ x2 tint_lt y)

⊢ ∀z y x. x tint_mul (y tint_mul z) = x tint_mul y tint_mul z

⊢ ∀x. tint_1 tint_mul x tint_eq x

⊢ ∀y x. x tint_mul y = y tint_mul x

⊢ ∀x1 x2 y1 y2.
    x1 tint_eq x2 ∧ y1 tint_eq y2 ⇒ x1 tint_mul y1 tint_eq x2 tint_mul y2

⊢ ∀x1 x2 y. x1 tint_eq x2 ⇒ x1 tint_mul y tint_eq x2 tint_mul y

⊢ ∀x1 x2. x1 tint_eq x2 ⇒ tint_neg x1 tint_eq tint_neg x2

⊢ (∀a. int_ABS_CLASS (int_REP_CLASS a) = a) ∧
  ∀c. (∃r. r tint_eq r ∧ c = $tint_eq r) ⇔
      int_REP_CLASS (int_ABS_CLASS c) = c

⊢ QUOTIENT $tint_eq int_ABS int_REP

⊢ &n + &m = &(n + m) ∧ -&n + &m = (if n ≤ m then &(m − n) else -&(n − m)) ∧
  &n + -&m = (if m ≤ n then &(n − m) else -&(m − n)) ∧
  -&n + -&m = -&(n + m) ∧ &n * &m = &(n * m) ∧ -&n * &m = -&(n * m) ∧
  &n * -&m = -&(n * m) ∧ -&n * -&m = &(n * m) ∧ (&n = &m ⇔ n = m) ∧
  (&n = -&m ⇔ n = 0 ∧ m = 0) ∧ (-&n = &m ⇔ n = 0 ∧ m = 0) ∧
  (-&n = -&m ⇔ n = m) ∧ --x = x ∧ -0 = 0

⊢ ∀x. (∃n. x = &n) ∨ ∃n. n ≠ 0 ∧ x = -&n

⊢ ∀b a. a int_divides b ⇔ ∃x. b = a * x

⊢ ∀n m. (&n = -&m ⇔ n = 0 ∧ m = 0) ∧ (-&n = &m ⇔ n = 0 ∧ m = 0)

⊢ a divides b ⇔ &a int_divides &b

⊢ ∀i. Num i = @n. if 0 ≤ i then i = &n else i = -&n

⊢ ∀n. FST (tint_of_num n) = SND (tint_of_num n) + n