Theorem add_com n m : n + m = m + n.
Proof.
  revert m.
  induction n as [|n IHn].
  - intros m.
    simpl.
    induction m as [|m IHm].
    + simpl. trivial.
    + simpl. rewrite <- IHm. reflexivity.
  - intros m.
    induction m as [|m IHm].
    + simpl.
      rewrite IHn. simpl. reflexivity.
    + simpl.
      rewrite IHn.
      simpl.
      rewrite <- IHm.
      simpl.
      rewrite IHn.
      reflexivity.
Qed.

Prove the following theorems; replace Abort command with Qed. If theorem A (including add_com) appears before theorem B in this file, you can use A to prove B.

Theorem add_assoc : forall x y z : nat, x + (y + z) = (x + y) + z.
Proof.
Abort.

Theorem mul_com' : forall x y : nat, x * y = y * x.
Proof.
Abort.

Fixpoint add' (n m : nat) :=
  match n with
  | O => m
  | S n' => add' n' (S m)
  end.

Lemma add'_S n m : add' n (S m) = S (add' n m).
Proof.
Abort.

Theorem add'_comm : forall n m, add' n m = add' m n.
Proof.
Abort.

Theorem plus'_assoc : forall n m k, add' n (add' m k) = add' (add' n m) k.
Proof.
Abort.

Theorem add'_add : forall n m, add' n m = n + m.
Proof.
Abort.