theorem linearEq :
  (a b c : Int) → (a - b < c) → (c + b > a) :=
  by omega

-- double negation elimination and excluded middle are equivalent
theorem doubleNegationEqEm :
  (¬¬p ↔ p) ↔ (p ∨ ¬p) :=
  by grind