plus_comm.v

Theorem plus_comm : forall n m : nat,
  n + m = m + n.
Proof.
  intros.
  induction n.

    induction m.
    reflexivity.
    simpl.  rewrite <- IHm. simpl. reflexivity.

  induction m.

    simpl. rewrite -> IHn. simpl. reflexivity.
    simpl.  rewrite <- IHm. 
      simpl. rewrite -> IHn. simpl. 
      induction n.
        simpl. 
        assert (plus_0_nat :forall l : nat, l + 0 = l).
          induction l. reflexivity. simpl. rewrite -> IHl. reflexivity.
        rewrite -> plus_0_nat. reflexivity.
  simpl. 
  assert (plus_Sm_n : forall n' m' : nat, m' + S n' = S n' + m').
  induction n'.
    induction m'.
      simpl. reflexivity.
      simpl. rewrite -> IHm'. simpl. reflexivity.
  induction m'.
    simpl. assert (plus_0_nat :forall l : nat, l + 0 = l).
            induction l. reflexivity. simpl. rewrite -> IHl. reflexivity.
  rewrite -> plus_0_nat. reflexivity.