Theorems
⊢ -&m + &m = 0 ∧ &m + -&m = 0
⊢ -&m + -&n = -&(m + n) ∧ -&m + &(m + n) = &n ∧ -&(m + n) + &m = -&n ∧
&(m + n) + -&m = &n ∧ &m + -&(m + n) = -&n ∧ &m + &n = &(m + n)
⊢ (&m = &n ⇔ m = n) ∧ (-&m = -&n ⇔ m = n) ∧ (-&m = &n ⇔ m = 0 ∧ n = 0) ∧
(&m = -&n ⇔ m = 0 ∧ n = 0)
⊢ (&m ≥ -&n ⇔ T) ∧ (&m ≥ &n ⇔ n ≤ m) ∧ (-&m ≥ -&n ⇔ m ≤ n) ∧
(-&m ≥ &n ⇔ m = 0 ∧ n = 0)
⊢ (-&m > &n ⇔ F) ∧ (&m > &n ⇔ n < m) ∧ (-&m > -&n ⇔ m < n) ∧
(&m > -&n ⇔ ¬(m = 0 ∧ n = 0))
⊢ (-&m ≤ &n ⇔ T) ∧ (&m ≤ &n ⇔ m ≤ n) ∧ (-&m ≤ -&n ⇔ n ≤ m) ∧
(&m ≤ -&n ⇔ m = 0 ∧ n = 0)
⊢ (F ∧ F ⇔ F) ∧ (F ∧ T ⇔ F) ∧ (T ∧ F ⇔ F) ∧ (T ∧ T ⇔ T)
⊢ (&m < -&n ⇔ F) ∧ (&m < &n ⇔ m < n) ∧ (-&m < -&n ⇔ n < m) ∧
(-&m < &n ⇔ ¬(m = 0 ∧ n = 0))
⊢ 0 * &x = 0 ∧ 0 * -&x = 0 ∧ &x * 0 = 0 ∧ -&x * 0 = 0
⊢ (&m * &n = &(m * n) ∧ -&m * -&n = &(m * n)) ∧ -&m * &n = -&(m * n) ∧
&m * -&n = -&(m * n)
⊢ &x ** n = &(x ** n) ∧ -&x ** n = if EVEN n then &(x ** n) else -&(x ** n)
⊢ (if T then x else y) = x ∧ (if F then x else y) = y