Inductive nat : Set :=
   | O : nat
   | S : nat -> nat.

 Require Import Coq.Arith.Plus.

 Definition mult_comm : forall n m, n * m = m * n.
 Proof.
 intros. elim n.
 auto with arith.
 intros. simpl in |- *. elim mult_n_Sm. elim H. apply plus_comm.
 Qed.

 Definition mult_comm := fun n:nat
 => fix rec (m : nat)
 : n * m = m * n
 := match m as m return n * m = m * n with
   | O => sym_eq (mult_n_O _)
   | S pm => match rec pm in _ = dep return _ = n + dep
     with refl_equal =>
       match mult_n_Sm _ _ in _ = dep return dep = _
       with refl_equal => plus_comm _ _ end
     end
   end.

 Definition mult_comm := fun n:nat
 => nat_ind (fun m => n * m = m * n)
   (sym_eq (mult_n_O _))
   (fun _ rec =>
     eq_ind _ (fun dep => _ = n + dep)
     (eq_ind _ (fun dep => dep = _)
       (plus_comm _ _) _ (mult_n_Sm _ _))
     _ rec).