Coqで加算の可換性の証明

gistfile1.txt

Lemma plus_a_0 : forall n : nat, n + 0 = n.
Proof.
  intros.
  induction n.
  simpl.
  reflexivity.
  simpl.
  rewrite IHn.
  reflexivity.
Qed.  
Lemma plus_0_a: forall n : nat, 0 + n = n.
Proof.
  intros.
  simpl.
  reflexivity.
Qed.

Lemma plus_S_m_n: forall n m : nat, S n + m = S ( n + m ). 
Proof.
  intros.
  simpl.
  reflexivity.
Qed.

Lemma plus_m_S_n: forall n m : nat, n + S m = S ( n + m).
Proof.
  intros.
  induction n.
  simpl.
  reflexivity.
  simpl.
  rewrite IHn.
  reflexivity.
Qed.

Theorem plus_a_b : forall n m : nat, n + m = m + n.
Proof.  
  intros.
  induction n.
  rewrite plus_0_a.
  rewrite plus_a_0.
  reflexivity.
  rewrite plus_S_m_n.
  rewrite plus_m_S_n.
  apply f_equal.
  exact IHn.
Qed.