Module NatPlayground.

  Inductive nat : Type :=
  | O
  | S (n : nat).

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

  Theorem right_S: forall n m : nat, plus n (S m) = S (plus n m).
  Proof.
    intros n m.
    induction n as [|n' IH].
    - simpl.
      reflexivity.
    - simpl.
      rewrite -> IH.
      reflexivity.
      Qed.
  Theorem conm: forall n m : nat, plus n m = plus m n.
  Proof.
    intros n m.
    induction n as [|n' IHn'].
    - induction m as [|m' IHm'].
    + (* m == O *) simpl.
      reflexivity.
    + (* m == S m' *)
      simpl.
      rewrite <- IHm'.
      reflexivity.
    - (* n == S n' *)                                                  
      simpl.
      rewrite -> IHn'.
      rewrite -> right_S.
      reflexivity.
      Qed.
End NatPlayground.