Set: pp::colors
  Set: pp::unicode
2
3
  Defined: x
2
⊤
  Assumed: y
if ℤ (0 ≤ -3 + y) (-3 + y) (-1 * (-3 + y))
| x + y | > x
  Set: lean::pp::notation
Int::gt (Int::abs (Int::add x y)) x
Int::gt (Int::add (Int::abs (Int::add x y)) (Int::abs (Int::add y x))) x