From 0d95f92e4a6243d46c437df45c00c0fe8e791acc Mon Sep 17 00:00:00 2001
From: Dmitriy Gorshenin <dmitriy.gorshenin@gmail.com>
Date: Thu, 2 Jun 2022 19:37:58 +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

---
 RingMult | 24 ------------------------
 1 file changed, 24 deletions(-)
 delete mode 100644 RingMult

diff --git a/RingMult b/RingMult
deleted file mode 100644
index 537eb43..0000000
--- a/RingMult
+++ /dev/null
@@ -1,24 +0,0 @@
- Record int_bipart : Set := {pneg : nat; ppos : nat}.
-
-
-
- Notation "a !+ b" := (Peano.plus a b) (at level 50, left associativity).
- Definition plus a b := Build_int_bipart
-   (pneg a !+ pneg b) (ppos a !+ ppos b).
- Notation "a + b" := (plus a b).
-
-Definition int_bipart_eq_part
-   : forall an bn, an = bn -> forall ap bp, ap = bp
-   -> Build_int_bipart an ap = Build_int_bipart bn bp.
- Proof.
- refine (fun _ _ eqn _ _ eqp => _).
- refine (eq_ind _ (fun n => _ = Build_int_bipart n _) _ _ eqn).
- refine (f_equal _ eqp).
- Qed.
-
- Require Import ArithRing.
- 
- Definition mult_comm : forall n m, n * m = m * n.
- Proof.
- refine (fun n m => int_bipart_eq_part _ _ _ _ _ _); simpl; ring.
- Qed.