14 lines
270 B
Text
14 lines
270 B
Text
|
Set: pp::colors
|
|||
|
|
Set: pp::unicode
|
|||
|
|
2
|
|||
|
|
3
|
|||
|
|
Defined: x
|
|||
|
|
2
|
|||
|
|
⊤
|
|||
|
|
Assumed: y
|
|||
|
|
ite Int (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
|