Require Export Relation_Definitions.
Require Coq.Arith.Plus.
Require Import ArithRing.

Record int_bipart : Set := {pneg : nat; ppos : nat}.

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.

Definition blank_0 blank := Build_int_bipart blank blank.

Definition no_blank_0 := blank_0 0.

Definition nat2int_bipart absolute := Build_int_bipart 0 absolute.

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).

Notation "a !* b" := (Peano.mult a b) (at level 40, left associativity).
Definition mult a b := Build_int_bipart
        (pneg a !* ppos b !+ ppos a !* pneg b)
        (pneg a !* pneg b !+ ppos a !* ppos b).
Notation "a * b" := (mult a b) (at level 40, left associativity).

Definition plus_0_l : forall n, no_blank_0 + n = n.

Definition plus_comm : forall n m, n + m = m + n.

Definition plus_assoc : forall n m p, n + (m + p) = (n + m) + p.

Definition mult_1_l : forall n, (nat2int_bipart 1) * n = n.

Definition mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p.

Definition mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p.

Definition mult_comm : forall n m, n * m = m * n.

Definition mult_assoc : forall n m p, n * (m * p) = n * m * p.

Definition opp a := Build_int_bipart (ppos a) (pneg a).
        Notation "- a" := (opp a).
Notation "a !- b" := (Peano.minus a b) (at level 50, left associativity).
        Definition minus a b := a + (-b).
        Notation "a - b" := (minus a b).

Definition opp_involution : forall n, n = - (- n).

Definition opp_plus : forall n m, - (n + m) = - m + - n.

Definition is0 a := ppos a = pneg a.

Check fun blank => (refl_equal _) : is0 (blank_0 blank).

Definition int_bipart_eq a b := is0 (- a + b).
Notation "a -= b" := (int_bipart_eq a b) (at level 70, no associativity).

Check fun n => (refl_equal _) : is0 n = (no_blank_0 -= n).

Definition is0_opp : forall n, is0 n <-> is0 (- n).

Definition minus_diag : forall n, is0 (n - n).

Definition int_bipart_eq_refl : reflexive _ int_bipart_eq.

Definition int_bipart_eq_trans : transitive _ int_bipart_eq.

Definition int_bipart_eq_sym : symmetric _ int_bipart_eq.

Definition int_bipart_eq_equiv := (Build_equivalence _ _
        int_bipart_eq_refl int_bipart_eq_trans int_bipart_eq_sym
        ) : equivalence _ int_bipart_eq.

Add Relation int_bipart int_bipart_eq
        reflexivity proved by (int_bipart_eq_refl)
        symmetry proved by (int_bipart_eq_sym)
        transitivity proved by (int_bipart_eq_trans)
        as int_bipart_eq_rel.

Definition int_bipart_eq_std : inclusion _ (@eq _) int_bipart_eq.

Require Export Setoid.

Definition plus_eq_compat : forall a1 a2, a1 -= a2
        -> forall b1 b2, b1 -= b2
        -> a1 + b1 -= a2 + b2.

Add Morphism plus
with signature int_bipart_eq ==> int_bipart_eq ==> int_bipart_eq
as plus_mor.

Definition mult_eq_compat : forall a1 a2, a1 -= a2
        -> forall b1 b2, b1 -= b2
        -> a1 * b1 -= a2 * b2.

Add Morphism mult
with signature int_bipart_eq ==> int_bipart_eq ==> int_bipart_eq
as mult_mor.

Definition opp_compat : forall a1 a2, a1 -= a2 -> -a1 -= -a2.

Add Morphism opp
with signature int_bipart_eq ==> int_bipart_eq
as opp_mor.

Definition int_bipart_rt : ring_theory no_blank_0 (nat2int_bipart 1)
        plus mult minus opp int_bipart_eq.

Add Ring int_bipart_ring_name : int_bipart_rt.

Definition eq_nat (n : nat) (i : int_bipart) := ppos i = n !+ pneg i.

Definition eq_nat_equiv n i : eq_nat n i <-> nat2int_bipart n -= i.

Definition nat_ext_plus an ai bn bi
        : eq_nat an ai -> eq_nat bn bi -> eq_nat (an !+ bn) (ai + bi).

Definition nat_ext_mult an ai bn bi
        : eq_nat an ai -> eq_nat bn bi -> eq_nat (an !* bn) (ai * bi).

Definition nat_ext_is0 n i : eq_nat n i -> (~ IsSucc n <-> is0 i).