22 lines
363 B
Text
22 lines
363 B
Text
|
VISIT consume_args.lean
|
||
|
|
SYNC 9
|
||
|
|
import logic data.nat.basic
|
||
|
|
open nat eq.ops
|
||
|
|
|
||
|
|
definition a := true
|
||
|
|
|
||
|
|
theorem tst (a b c : nat) : a + b + c = a + c + b :=
|
||
|
|
calc a + b + c = a + (b + c) : _
|
||
|
|
... = a + (c + b) : {!add.comm}
|
||
|
|
... = a + c + b : (!add.assoc)⁻¹
|
||
|
|
WAIT
|
||
|
|
CLEAR_CACHE
|
||
|
|
WAIT 100
|
||
|
|
INFO 4
|
||
|
|
WAIT
|
||
|
|
INFO 4
|
||
|
|
FINDG 7 31
|
||
|
|
+assoc -symm
|
||
|
|
WAIT
|
||
|
|
SLEEP 20
|
||
|
|
SHOW
|