Addition properties in Coq

addition.v

Lemma zero_addition_identity_right :
  forall x : nat, x + 0 = x.
Proof.
  intro x; induction x.
  - compute; reflexivity.
  - simpl; f_equal; apply IHx.
Qed.

Lemma zero_addition_identity_left :
  forall x : nat, x = x + 0.
Proof.
  intro x; induction x.
  - simpl; reflexivity.
  - simpl; f_equal; apply IHx.
Qed.

Lemma addition_distributive_S :
  forall n m : nat, S (m + n) = m + S n.
Proof.
  intros n m; induction m; simpl.
  - reflexivity.
  - rewrite IHm; reflexivity.
Qed.

Theorem addition_associative :
  forall a b c : nat, (a + b) + c = a + (b + c).
Proof.
  intros a b c; induction a; simpl.
  - reflexivity.
  - f_equal; apply IHa.
Qed.

Theorem addition_commutative :
  forall a b : nat, a + b = b + a.
Proof.
  intros a b; induction a; simpl.
  - apply zero_addition_identity_left.
  - rewrite IHa; apply addition_distributive_S.
Qed.