Коммутативность кольцевого умножения

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.