Theorem: LoVe.BackwardProofs.abc_Eq_cba (LoVe/Lectures/LoVe03_BackwardProofs_Demo.lean)

State before:
a b c : ℕ
⊢ a + b + c = c + b + a
Tactic:
ac_rfl
State after:
no goals