From ef96a75751275d805caa18fb6d5dbffdb6f041f7 Mon Sep 17 00:00:00 2001
From: Dmitriy Gorshenin <dmitriy.gorshenin@gmail.com>
Date: Thu, 2 Jun 2022 19:36:00 +0300
Subject: [PATCH] =?UTF-8?q?=20=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=D0=BA=D0=BE?=
 =?UTF-8?q?=D0=BB=D1=8C=D1=86=D0=B5=D0=B2=D0=BE=D0=B3=D0=BE=20=D1=83=D0=BC?=
 =?UTF-8?q?=D0=BD=D0=BE=D0=B6=D0=B5=D0=BD=D0=B8=D1=8F?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 RingMult.v | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 RingMult.v

diff --git a/RingMult.v b/RingMult.v
new file mode 100644
index 0000000..537eb43
--- /dev/null
+++ b/RingMult.v
@@ -0,0 +1,24 @@
+ 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.