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.