Theory intExtension

⊢ ∀x. SGN x = if x = 0 then 0 else if x < 0 then -1 else 1

⊢ ABS x = x * SGN x

⊢ ABS (SGN i) = if i = 0 then 0 else 1

⊢ ABS 0 = 0

⊢ ∀a. a < 0 ⇒ ABS a = -a

⊢ ∀a. 0 < a ⇒ ABS a = a

⊢ ∀p. p ≠ 0 ⇒ 0 < ABS p

⊢ ∀a b n. 0 < n ⇒ (a = b ⇔ a * n = b * n)

⊢ ∀a. 0 < a ⇒ a ≠ 0

⊢ ∀a b n. 0 < n ⇒ (a > b ⇔ a * n > b * n)

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

⊢ ∀a b n. 0 < n ⇒ (a < b ⇔ a * n < b * n)

⊢ ∀a b. 0 < a ⇒ 0 < b ⇒ 0 < a * b

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

⊢ ∀a b. a ≠ 0 ⇒ b ≠ 0 ⇒ a * b ≠ 0

⊢ ∀x. x ≠ 0 ⇒ SGN x ≠ 0

⊢ ∀n. ¬(n < 0) ⇔ 0 = n ∨ 0 < n

⊢ ∀a. ¬(a < 0) ⇒ a ≠ 0 ⇒ 0 < a

⊢ ∀a. ¬(0 < a) ⇒ a ≠ 0 ⇒ 0 < -a

⊢ ∀a P.
    (SGN a = -1 ∧ a < 0 ⇒ P) ∧ (SGN a = 0 ∧ a = 0 ⇒ P) ∧
    (SGN a = 1 ∧ 0 < a ⇒ P) ⇒
    P

⊢ ∀x. (SGN x = -1 ⇔ x < 0) ∧ (SGN x = 0 ⇔ x = 0) ∧ (SGN x = 1 ⇔ 0 < x)

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

⊢ ∀x. SGN x ≠ -1 ⇒ SGN x ≠ 1 ⇒ SGN x = 0

⊢ ∀a. SGN a = -1 ∨ SGN a = 0 ∨ SGN a = 1

⊢ ∀n. 0 < n ⇒ n ≠ 0

⊢ ABS x * SGN x = x

⊢ SGN i * &Num i = i