Коммутативность умножения в арифметике Пеано

KompFunc

@@ -1,8 +0,0 @@
- Definition cf := fun t0 t1 t2 : Type
-   => fun (f : t1 -> t2) (g : t0 -> t1) => fun x => f (g x).
- Implicit Arguments cf [t0 t1 t2].
- Notation "f @ g" := (cf f g) (at level 65, left associativity).
- 
- Definition cf_assoc := fun (t0 t1 t2 t3 : Type)
-   (f : t2 -> t3) (g : t1 -> t2) (h : t0 -> t1)
-   => (refl_equal _) : (f @ g) @ h = f @ (g @ h).

PeanoMult.v

@@ -0,0 +1,34 @@
+ 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).
+