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.