Lemma assoc_a :
  forall a b c d : nat,
    ((a + b) + c) + d = a + (b + (c + d)).
Proof.
  intros a b c d.

  rewrite -> (plus_assoc a b (c + d)).
  rewrite -> (plus_assoc (a + b) c d).
  reflexivity.
Qed.