A simple proof, hope it works

import Mathlib

theorem testing : ∀ a b c d e : Nat, a + b + c + d + e = (c + (e + d)) + (b + a) := by
  intros
  abel