Theory normalizer

⊢ 0 < n ⇒
  P (m DIV n) (m MOD n) ∧ (∀q r. (m ≠ q * n + r ∨ ¬(r < n)) ∨ P q r) ∨
  ¬P (m DIV n) (m MOD n) ∧ ∃q r. (m = q * n + r ∧ r < n) ∧ ¬P q r

⊢ ∀n. ¬EVEN n ⇔ ODD n

⊢ ∀n. ¬ODD n ⇔ EVEN 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

⊢ w = x + d ∧ y = z + e ⇒ (w * y + x * z = w * z + x * y ⇔ w = x ∨ y = z)

⊢ 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² ∧
  (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

⊢ (EVEN x ⇔ ∀y. x ≠ SUC (2 * y)) ∧ (ODD x ⇔ ∀y. x ≠ 2 * y) ∧
  (¬EVEN x ⇔ ∀y. x ≠ 2 * y) ∧ (¬ODD x ⇔ ∀y. x ≠ SUC (2 * y))

⊢ P (PRE n) ⇔ ∀m. n ≠ SUC m ∧ (m ≠ 0 ∨ n ≠ 0) ∨ P m

⊢ (p ⇒ F) ⇒ (¬q ⇔ p) ⇒ q

⊢ ∀add mul n0.
    (∀x. mul n0 x = n0) ∧ (∀x y z. add x y = add x z ⇔ y = z) ∧
    (∀w x y z.
       add (mul w y) (mul x z) = add (mul w z) (mul x y) ⇔ w = x ∨ y = z) ⇒
    (∀a b c d.
       a ≠ b ∧ c ≠ d ⇔ add (mul a c) (mul b d) ≠ add (mul a d) (mul b c)) ∧
    ∀n a b c d. n ≠ n0 ⇒ a = b ∧ c ≠ d ⇒ add a (mul n c) ≠ add b (mul n d)

⊢ (∀x y z. add x (add y z) = add (add x y) z) ∧ (∀x y. add x y = add y x) ∧
  (∀x. add r0 x = x) ∧ (∀x y z. mul x (mul y z) = mul (mul x y) z) ∧
  (∀x y. mul x y = mul y x) ∧ (∀x. mul r1 x = x) ∧ (∀x. mul r0 x = r0) ∧
  (∀x y z. mul x (add y z) = add (mul x y) (mul x z)) ∧
  (∀x. pwr x 0 = r1) ∧ (∀x n. pwr x (SUC n) = mul x (pwr x n)) ⇒
  mul r1 x = x ∧ add (mul a m) (mul b m) = mul (add a b) m ∧
  add (mul a m) m = mul (add a r1) m ∧ add m (mul a m) = mul (add a r1) m ∧
  add m m = mul (add r1 r1) m ∧ mul r0 m = r0 ∧ add r0 a = a ∧
  add a r0 = a ∧ mul a b = mul b a ∧
  mul (add a b) c = add (mul a c) (mul b c) ∧ mul r0 a = r0 ∧
  mul a r0 = r0 ∧ mul r1 a = a ∧ mul a r1 = a ∧
  mul (mul lx ly) (mul rx ry) = mul (mul lx rx) (mul ly ry) ∧
  mul (mul lx ly) (mul rx ry) = mul lx (mul ly (mul rx ry)) ∧
  mul (mul lx ly) (mul rx ry) = mul rx (mul (mul lx ly) ry) ∧
  mul (mul lx ly) rx = mul (mul lx rx) ly ∧
  mul (mul lx ly) rx = mul lx (mul ly rx) ∧ mul lx rx = mul rx lx ∧
  mul lx (mul rx ry) = mul (mul lx rx) ry ∧
  mul lx (mul rx ry) = mul rx (mul lx ry) ∧
  add (add a b) (add c d) = add (add a c) (add b d) ∧
  add (add a b) c = add a (add b c) ∧ add a (add c d) = add c (add a d) ∧
  add (add a b) c = add (add a c) b ∧ add a c = add c a ∧
  add a (add c d) = add (add a c) d ∧
  mul (pwr x p) (pwr x q) = pwr x (p + q) ∧
  mul x (pwr x q) = pwr x (SUC q) ∧ mul (pwr x q) x = pwr x (SUC q) ∧
  mul x x = pwr x 2 ∧ pwr (mul x y) q = mul (pwr x q) (pwr y q) ∧
  pwr (pwr x p) q = pwr x (p * q) ∧ pwr x 0 = r1 ∧ pwr x 1 = x ∧
  mul x (add y z) = add (mul x y) (mul x z) ∧
  pwr x (SUC q) = mul x (pwr x q)

⊢ P (a − b) ⇔ ∀d. a ≠ b + d ∧ (¬(a < b) ∨ d ≠ 0) ∨ P d