From ab63ebcf527cb2919a03ecfd99345c07059c4664 Mon Sep 17 00:00:00 2001
From: Dmitriy Gorshenin <dmitriy.gorshenin@gmail.com>
Date: Thu, 2 Jun 2022 19:41:02 +0300
Subject: [PATCH] =?UTF-8?q?=D0=A3=D0=B4=D0=B0=D0=BB=D0=B5=D0=BD=D0=B8?=
 =?UTF-8?q?=D0=B5=20=D1=84=D0=B0=D0=B9=D0=BB=D0=B0?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 PeanoMult | 34 ----------------------------------
 1 file changed, 34 deletions(-)
 delete mode 100644 PeanoMult

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