VISIT consume_args.lean
SYNC 7
import logic data.nat.basic
open nat eq.ops algebra

theorem tst (a b c : nat) : a + b + c = a + c + b :=
calc a + b + c = a + (b + c) : by rewrite add.assoc
         ...   = a + (c + b) : by rewrite (add.comm b c)
         ...   = a + c + b   : by rewrite add.assoc
WAIT
INFO 7