2013-09-04 03:39:54 +00:00
|
|
|
|
Set: pp::colors
|
|
|
|
|
Set: pp::unicode
|
|
|
|
|
2
|
|
|
|
|
3
|
|
|
|
|
Defined: x
|
|
|
|
|
2
|
|
|
|
|
⊤
|
|
|
|
|
Assumed: y
|
2013-09-04 16:03:41 +00:00
|
|
|
|
if ℤ (0 ≤ -3 + y) (-3 + y) (-1 * (-3 + y))
|
2013-09-04 03:39:54 +00:00
|
|
|
|
| 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
|