Theorem plus_comm: ∀ n m : ℕ, n + m = m + n

Proof:
  intros n m.
  induction n as [| n' IH].
  - (* Base case: n = 0 *)
    simpl.
    rewrite plus_0_r.
    reflexivity.
  - (* Inductive case: n = S n' *)
    simpl.
    rewrite IH.
    rewrite plus_n_Sm.
    reflexivity.
Qed.