From c72b9853172dbcc2951b5cefbdb37d8714208c80 Mon Sep 17 00:00:00 2001
From: Dmitriy Gorshenin <dmitriy.gorshenin@gmail.com>
Date: Tue, 31 May 2022 22:45:39 +0300
Subject: [PATCH] =?UTF-8?q?=D0=9A=D0=BE=D0=BC=D0=BC=D1=83=D1=82=D0=B0?=
 =?UTF-8?q?=D1=82=D0=B8=D0=B2=D0=BD=D0=BE=D1=81=D1=82=D1=8C=20=D1=83=D0=BC?=
 =?UTF-8?q?=D0=BD=D0=BE=D0=B6=D0=B5=D0=BD=D0=B8=D1=8F=20=D0=B2=20=D0=B0?=
 =?UTF-8?q?=D1=80=D0=B8=D1=84=D0=BC=D0=B5=D1=82=D0=B8=D0=BA=D0=B5=20=D0=9F?=
 =?UTF-8?q?=D0=B5=D0=B0=D0=BD=D0=BE?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 PeanoMult | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)
 create mode 100644 PeanoMult

diff --git a/PeanoMult b/PeanoMult
new file mode 100644
index 0000000..5d626a2
--- /dev/null
+++ b/PeanoMult
@@ -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).
+