(* compiles with COQ 8.7*)
Theorem nsr_plus_associative: forall a b c:nat, a+(b+c) = (a+b)+c.
Proof.
  induction a.
  intros.
  simpl.
  reflexivity.
  intros.
  simpl.
  rewrite IHa.
  reflexivity.
Qed.

Theorem nsr_plus_commutative: forall x y:nat, x+y = y + x.
Proof.
  induction x.
  intro.
  rewrite <-plus_n_O.
  simpl.
  reflexivity.
  intro.
  simpl.
  rewrite <-plus_n_Sm.
  rewrite IHx.
  reflexivity.
Qed.

Theorem nsr_right_distributivity: forall x y z:nat, (x+y)*z = (x*z)+(y*z).
Proof.
  induction x.
  simpl.
  reflexivity.
  simpl.
  intros.
  assert (z+  x * z + y * z = z + (x * z + y * z)).
  apply eq_sym.
  apply nsr_plus_associative.
  rewrite H.
  apply f_equal.
  apply IHx.
Qed.

Theorem nsr_mult_commutative: forall x y:nat, x*y = y*x.
Proof.
  induction x.
  simpl.
  intro.
  rewrite <- mult_n_O.
  reflexivity.
  simpl.
  assert (forall a b:nat, b * (S a) = b + b * a).
  induction b.
  simpl.
  reflexivity.
  simpl.
  rewrite IHb.
  apply f_equal.
  rewrite nsr_plus_associative.
  rewrite nsr_plus_associative.
  rewrite nsr_plus_commutative with (x:=a) (y:=b).
  reflexivity.
  intro.
  apply eq_sym.
  rewrite IHx.
  apply H.
Qed.

Theorem nsr_left_distributivity: forall x y z:nat, z*(x+y) = (z*x)+(z*y).
Proof.
  intros.
  rewrite nsr_mult_commutative with (x:=z) (y:=x+y).
  rewrite nsr_mult_commutative with (x:=z) (y:=x).
  rewrite nsr_mult_commutative with (x:=z) (y:=y).
  apply nsr_right_distributivity.
Qed.
    
Theorem nsr_mult_associative: forall x y z:nat, x*(y*z)=(x*y)*z.
Proof.
  induction x.
  intros.
  simpl.
  reflexivity.
  simpl.
  intros.
  rewrite nsr_right_distributivity.
  rewrite IHx.
  reflexivity.
Qed.

Theorem nsr_O_absorbs: forall n:nat, 0 * n = 0.
Proof.
  intros.
  simpl.
  reflexivity.
Qed.

Theorem nsr_I_mult_neutral: forall n:nat, 1 * n = n.
Proof.
  cut(forall n:nat,  n * 1 =n ).
  intros.
  rewrite nsr_mult_commutative.
  apply H.
  induction n.
  simpl.
  reflexivity.
  simpl.
  rewrite IHn.
  reflexivity.
Qed.

Theorem nsr_O_plus_neutral: forall n:nat, n = 0 + n.
Proof.
  intros.
  simpl.
  reflexivity.
Qed.

Lemma nat_sum_regularity: forall x y z:nat, x+ y = x + z -> y = z.
Proof.
  induction x.
  simpl.
  intros.
  assumption.
  intro.
  intro.
  rewrite plus_Sn_m.  
  rewrite plus_Sn_m.
  intro.
  apply IHx.
  apply eq_add_S.
  assumption.
Qed.

Lemma eq_prod: forall a a' b b':nat, a=a' -> b=b' -> (a,b)=(a',b').
  Proof.
    intros.
    rewrite H.
    rewrite H0.
    reflexivity.
Qed.
    
Notation Relative_integer := (prod nat nat).

Definition eqz (a b:Relative_integer):Prop := fst a + snd b = fst b + snd a.

Lemma eqz_reflexive: forall a:Relative_integer, eqz a a.
Proof.
  intro.
  destruct a.
  unfold eqz.
  reflexivity.
Qed.

Lemma eqz_symmetric: forall a b:Relative_integer, eqz a b -> eqz b a.
Proof.
  unfold eqz.
  intros.
  rewrite H.
  reflexivity.
Qed.

Lemma eqz_transitive: forall a b c:Relative_integer, eqz a b -> eqz b c -> eqz a c.
Proof.
  unfold eqz.
  intro.
  intro.
  intro.
  destruct a as (p_a,q_a).
  destruct b as (p_b,q_b).
  destruct c as (p_c,q_c).
  simpl.
  intros.
  apply nat_sum_regularity with (x:= q_b).
  rewrite nsr_plus_associative.
  rewrite nsr_plus_associative.
  assert (q_b+p_a=p_a+q_b).
  apply nsr_plus_commutative.
  rewrite H1.
  rewrite H.
  assert (q_b + p_c = p_c + q_b).
  apply nsr_plus_commutative.
  rewrite H2.
  rewrite <- H0.
  rewrite <- nsr_plus_associative.
  rewrite <- nsr_plus_associative.
  apply f_equal.
  apply nsr_plus_commutative.
Qed.
  
Definition Z_plus (a b:Relative_integer):Relative_integer := (fst a + fst b, snd a + snd b).
Definition Z_zero:Relative_integer:= (0,0).
Definition Z_un:Relative_integer:= (1,0).

Lemma Z_plus_associative_equal:
  forall (a b c:Relative_integer), Z_plus a (Z_plus b c) = Z_plus (Z_plus a b) c.
Proof.
  intro.
  destruct a as (p_a,q_a).
  intro.
  destruct b as (p_b,q_b).
  intro.
  destruct c as (p_c,q_c).
  unfold Z_plus.
  simpl.
  assert (forall u v w x:nat, u=w -> v = x -> (u,v)=(w,x)) as LEMMA.
  intros.
  rewrite H.
  rewrite H0.
  reflexivity.
  apply LEMMA.
  apply nsr_plus_associative.
  apply nsr_plus_associative.
Qed.

Theorem Z_plus_associative: forall (a b c:Relative_integer),
    eqz ( Z_plus a (Z_plus b c)) ( Z_plus (Z_plus a b) c).
  Proof.
  intros.
  rewrite Z_plus_associative_equal.
  apply eqz_reflexive.
Qed.

Notation "a +Z b":= (Z_plus a b) (left associativity, at level 61).
Notation "a =Z b":= (eqz a b) (left associativity, at level 71).  

Definition Z_mult (x y:Relative_integer):Relative_integer:=
  ((fst x)*(fst y) + (snd x)* (snd y), (fst x)*(snd y)+(snd x)*(fst y)). 

Notation "a *Z b":= (Z_mult a b) (left associativity, at level 59).

(*the following are abreviations used in manually done computations *)
Ltac arl p q r := rewrite nsr_plus_associative with (a:=p) (b:=q) (c:=r). 
Ltac alr p q r := rewrite <- nsr_plus_associative with (a:=p) (b:=q) (c:=r). 
Ltac com p q := rewrite nsr_plus_commutative with (x:= p) (y:=q).

Ltac mrl p q r := rewrite nsr_mult_associative with (x:=p) (y:=q) (z:=r). 
Ltac mlr p q r := rewrite <- nsr_mult_associative with (x:=p) (y:=q) (z:=r). 
Ltac mom p q := rewrite nsr_mult_commutative with (x:= p) (y:=q).

Ltac dir p q r := rewrite nsr_right_distributivity with (x:=p) (y:=q)(z:=r).
Ltac dil p q r := rewrite nsr_left_distributivity with (x:=q) (y:=r) (z:=p).
Ltac fir p q r := rewrite <- nsr_right_distributivity with (x:=p) (y:=q)(z:=r).
Ltac fil p q r := rewrite <- nsr_left_distributivity with (x:=q) (y:=r) (z:=p).
 

Theorem Z_mult_associative: forall x y z:Relative_integer, x *Z (y *Z z) =Z x *Z y *Z z. 
Proof.
  intro.
  destruct x as (a,b).
  intro.
  destruct y as (c,d).
  intro.
  destruct z as (e,f).
  unfold Z_mult.
  unfold eqz.
  simpl.
  rewrite nsr_left_distributivity with (z:=a) (x:=c * e) (y:= d * f).
  rewrite nsr_mult_associative with (x:= a) (y:=c) (z:=e).
  rewrite nsr_mult_associative with (x:= a) (y:=d) (z:=f).
  rewrite nsr_left_distributivity with (z:=b) (x:=c * f) (y:= d * e).
  rewrite nsr_mult_associative with (x:= b) (y:=c) (z:=f).
  rewrite nsr_mult_associative with (x:= b) (y:=d) (z:=e).
  rewrite nsr_left_distributivity with (z:=a) (x:=c * f) (y:= d * e).
  rewrite nsr_mult_associative with (x:= a) (y:=c) (z:=f).
  rewrite nsr_mult_associative with (x:= a) (y:=d) (z:=e).
  rewrite nsr_left_distributivity with (z:=b) (x:=c * e) (y:= d * f).
  rewrite nsr_mult_associative with (x:= b) (y:=c) (z:=e).
  rewrite nsr_mult_associative with (x:= b) (y:=d) (z:=f).
  rewrite nsr_right_distributivity with (x:= a * c) (y:= b * d) (z:=f).
  rewrite nsr_right_distributivity with (x:= a * d) (y:= b * c) (z:=e).
  rewrite nsr_right_distributivity with (x:= a * c) (y:= b * d) (z:=e).
  rewrite nsr_right_distributivity with (x:= a * d) (y:= b * c) (z:=f).
  assert (forall (ace adf bcf bde acf bdf ade bce:nat),
             ace + adf + (bcf + bde) + (acf + bdf + (ade + bce)) =
         ace + bde + (adf + bcf) + (acf + ade + (bce + bdf))) as L.
  intros.
  com bcf bde.
  alr ace adf (bde + bcf). 
  arl adf bde bcf.
  com adf bde.
  alr ace bde (adf + bcf).
  alr bde adf bcf.
  com bce bdf.
  arl (acf + ade) bdf bce.
  alr acf ade bdf.
  com ade bdf.
  arl acf bdf ade.
  alr (acf + bdf) ade bce.
  reflexivity.  
  apply L.
Qed.

Theorem Z_plus_commutative: forall a b:Relative_integer, a +Z b =Z b +Z a.
Proof.
  intros.
  unfold eqz.
  unfold Z_plus.
  simpl.
  com (fst a) (fst b).
  com (snd a) (snd b).
  reflexivity.
Qed.

Theorem Z_mult_commutative: forall a b:Relative_integer, a *Z b =Z b *Z a.
Proof.
  intros.
  unfold eqz.
  unfold Z_mult.
  simpl.
  mom (fst a) (fst b).
  mom (snd a) (snd b).
  mom (fst a) (snd b).
  mom (fst b) (snd a).
  com (snd a * fst b) (snd b * fst a).
  reflexivity.  
Qed.

Theorem Z_right_distributivity: forall a b c:Relative_integer, (a +Z b) *Z c =Z (a *Z c) +Z (b *Z c).
Proof.
  intros.
  destruct a as (p,q).
  destruct b as (r,s).
  destruct c as (t,u).
  unfold eqz.
  unfold Z_plus.
  unfold Z_mult.
  simpl.
  dir p r t.
  dir q s u.
  dir p r u.
  dir q s t.
  assert (forall (a b c d:nat), a + b + (c + d) = a + c + (b + d)) as L.
  intros.
  alr a b (c+d).
  arl b c d.
  com b c.
  alr c b d.
  arl a c (b + d).
  reflexivity.
  rewrite L with (a:= p * t) (b:= r * t) (c:= q * u) (d:= s * u).
  apply f_equal.
  apply L.
Qed.

Theorem Z_zero_plus_neutral: forall a:Relative_integer, Z_zero +Z a =Z a.
Proof.
  intro.
  unfold eqz.
  unfold Z_plus.
  unfold Z_zero.
  simpl.
  reflexivity.
Qed.

Notation O_Z:= (Z_zero).
Notation I_Z := (Z_un).

Theorem Z_un_neutral: forall a:Relative_integer, I_Z *Z a =Z a.
Proof.
  intros.
  destruct a as (x,y).
  unfold eqz.
  unfold Z_mult.
  unfold Z_un.
  simpl.
  alr x 0 0.
  alr x (0 + 0) y.
  com (0+0) y.
  arl y 0 0.
  reflexivity. 
Qed.

Definition Z_opp (a:Relative_integer):Relative_integer:= (snd a,fst a).
Definition Z_minus (a b:Relative_integer):Relative_integer:= ((fst a) + (snd b), (snd a)+ (fst b)).

Notation "a -Z b" := (Z_minus a b) (at level 69).

Theorem Z_opp_group: forall x:Relative_integer, x +Z (Z_opp x) =Z O_Z.
Proof.
  intros.
  destruct x as (p,q).
  unfold eqz.
  unfold Z_plus.
  unfold Z_opp.
  simpl.
  com p q.
  com (q + p) 0.
  simpl.
  reflexivity.
Qed.

Theorem Z_minus_opp: forall x y:Relative_integer, x -Z y =Z x +Z (Z_opp y).
Proof.
  intros.
  unfold eqz.
  unfold Z_plus.
  unfold Z_minus.
  unfold Z_opp.
  simpl.
reflexivity.
Qed.

Theorem Z_sum_compatibility: forall x x0 y y0:Relative_integer,
    x =Z y -> x0 =Z y0 -> (x +Z x0) =Z (y +Z y0).
Proof.
  intro.
  intro.
  intro.
  intro.
  unfold eqz.
  unfold Z_plus.
  destruct x as (a,b).
  destruct y as (c,d).
  destruct x0 as (e,f).
  destruct y0 as (g,h).
  simpl.
  intros.
  arl (a+e) d h.
  alr a e d.
  com e d.
  arl a d e.
  rewrite H.
  alr (c+b) e h.
  rewrite H0.
  arl (c + b) g f.
  arl (c + g) b f.
  alr c b g.
  alr c g b.
  com b g.
  reflexivity.
Qed.

Theorem Z_mult_compatibility: forall x x0 y y0:Relative_integer,
    x =Z y -> x0 =Z y0 -> (x *Z x0) =Z (y *Z y0).
Proof.
  assert (forall p q r:Relative_integer, eqz p q -> eqz (p *Z r) (q *Z r)) as L. 
  unfold eqz.
  unfold Z_mult.
  intro.
  intro.
  intro.
  destruct p as (a,b).
  destruct q as (c,d).
  destruct r as (x,y).
  simpl.
  intros.
  alr (a * x) (b * y) (c * y + d * x).
  arl (b * y) (c * y) (d * x).
  fir b c y.
  com b c.
  rewrite <- H.
  com (a * y) (b * x).
  com (c * x) (d * y).
  alr (d * y) (c * x) (b * x + a * y).
  arl (c * x) (b * x) (a * y).
  fir c b x.
  rewrite <- H.
  dir a d x.
  dir a d y.
  alr (a * x) (d * x) (a * y).
  com (d * x) (a * y).
  arl (a * x) (a * y) (d * x).
  arl (d * y) (a * x + a * y) (d * x).
  arl (d * y) (a * x) (a * y).
  com (d * y) (a * x).
  alr (a * x) (d * y) (a * y).
  arl (a * x) (a * y + d * y) (d * x).
  com (a * y) (d * y).
  reflexivity.
  intros.
  apply eqz_transitive with (b:= y *Z x0).
  apply L.
  assumption.
  apply eqz_transitive with (b:= x0 *Z y).
  apply Z_mult_commutative.  
  apply eqz_transitive with (b:= y0 *Z y).
  apply L.
  assumption.
  apply Z_mult_commutative.
Qed.

Theorem Z_opp_compatibility: forall x y:Relative_integer, x =Z y -> Z_opp x =Z Z_opp y.
Proof.
  unfold eqz.
  unfold Z_opp.
  intros.
  simpl.
  rewrite nsr_plus_commutative.
  rewrite <- H.
  apply nsr_plus_commutative.
Qed.

Theorem Z_left_distributivity: forall a b c:Relative_integer, c *Z (a +Z b) =Z (c *Z a) +Z (c *Z b).
Proof.
  intros.
  apply eqz_transitive with (b:= (a +Z b) *Z c).
  apply Z_mult_commutative.
  apply eqz_transitive with (b:= (a *Z c)+Z (b *Z c)).
  apply Z_right_distributivity.
  apply Z_sum_compatibility.
  apply Z_mult_commutative.
  apply Z_mult_commutative.
Qed.

Theorem Z_sum_regularity: forall x y z:Relative_integer, x +Z z =Z y +Z z -> x =Z y.
Proof.
  intros.
  assert (forall p r:Relative_integer, p =Z (p +Z r) +Z (Z_opp r))as LEMMA1.
  intros.
  apply eqz_transitive with (b:= p +Z (r +Z (Z_opp r))).
  apply eqz_transitive with (b:= p +Z O_Z).
  apply eqz_transitive with (b:= O_Z +Z p).
  apply eqz_symmetric.
  apply Z_zero_plus_neutral.
  apply Z_plus_commutative.
  apply Z_sum_compatibility.
  apply eqz_reflexive.
  apply eqz_symmetric.
  apply Z_opp_group.
  apply Z_plus_associative.
  intros.
  apply eqz_transitive with (b:= (x +Z z) +Z (Z_opp z)).
  apply LEMMA1.
  apply eqz_transitive with (b:= (y +Z z) +Z (Z_opp z)).
  apply Z_sum_compatibility.
  assumption.
  apply eqz_reflexive.
  apply eqz_symmetric.
  apply LEMMA1.
Qed.

Theorem Z_zero_product:forall x:Relative_integer, x *Z O_Z =Z O_Z.
  (*we show this property is a consequence of ring axioms as coq intended them, rather
than using the specific structure of Relative_integer defined above*)
Proof.
  intros.
  apply Z_sum_regularity with (z:= x *Z I_Z).
  apply eqz_transitive with (b:= x *Z (O_Z +Z I_Z)).
  apply eqz_symmetric.
  apply Z_left_distributivity.
  apply eqz_transitive with (b:= x *Z I_Z).
  apply Z_mult_compatibility.
  apply eqz_reflexive.
  apply Z_zero_plus_neutral.
  apply eqz_symmetric.
  apply Z_zero_plus_neutral.
Qed.

Theorem sign_rule:forall x y:Relative_integer,
    (Z_opp x) *Z (Z_opp y) =Z x *Z y.
Proof.
  intros.
  assert (forall p r:Relative_integer, p =Z (p +Z r) +Z (Z_opp r))as LEMMA1.
  intros.
  apply eqz_transitive with (b:= p +Z (r +Z (Z_opp r))).
  apply eqz_transitive with (b:= p +Z O_Z).
  apply eqz_transitive with (b:= O_Z +Z p).
  apply eqz_symmetric.
  apply Z_zero_plus_neutral.
  apply Z_plus_commutative.
  apply Z_sum_compatibility.
  apply eqz_reflexive.
  apply eqz_symmetric.
  apply Z_opp_group.
  apply Z_plus_associative.
  assert (forall p q r:Relative_integer, p +Z r =Z q +Z r -> p =Z q) as LEMMA2.
  intros.
  apply eqz_transitive with (b:= (p +Z r) +Z (Z_opp r)).
  apply LEMMA1.
  apply eqz_transitive with (b:= (q +Z r) +Z (Z_opp r)).
  apply Z_sum_compatibility.
  assumption.
  apply eqz_reflexive.
  apply eqz_symmetric.
  apply LEMMA1.
  apply LEMMA2 with (r:= (Z_opp x) *Z y).
  apply eqz_transitive with (b:= O_Z).
  apply eqz_transitive with (b:= (Z_opp x) *Z ((Z_opp y +Z y))).
  apply eqz_symmetric.
  apply Z_left_distributivity.
  apply eqz_transitive with (b:= Z_opp x *Z O_Z).
  apply Z_mult_compatibility.
  apply eqz_reflexive.
  apply eqz_transitive with (b:= y +Z (Z_opp y)).
  apply Z_plus_commutative.
  apply Z_opp_group.
  apply Z_zero_product.
  apply eqz_transitive with (b:= O_Z *Z y).
  apply eqz_symmetric.
  apply eqz_transitive with (b:= y *Z O_Z).
  apply eqz_symmetric.
  apply Z_mult_commutative.
  apply Z_zero_product.
  apply eqz_transitive with (b:= (x +Z (Z_opp x)) *Z y).
  apply Z_mult_compatibility.
  apply eqz_symmetric.
  apply Z_opp_group.
  apply eqz_reflexive.
  apply Z_right_distributivity.
Qed.

Ltac zer := apply eqz_reflexive.
Ltac zes := apply eqz_symmetric.
Ltac zet p:= apply eqz_transitive with (b:=p).
Ltac zcom:= apply Z_mult_commutative.

Section Signs_of_relative_integers.
  Fixpoint zsign_nat (p q:nat):Relative_integer:=
    match p with
    |0 => match q with
          |0 => O_Z
          |S t => (0,1)
          end
    |S r => match q with
            |0 => I_Z
            |S u => zsign_nat r u
            end
    end.

  Definition zsign (x:Relative_integer):Relative_integer:= zsign_nat (fst x) (snd x).

  Lemma calc_AOO: forall x:nat, zsign_nat x x = O_Z.
  Proof.
    induction x.
    simpl.
    reflexivity.
    simpl.
    apply IHx.
  Qed.

  Lemma calc_AOS: forall x y:nat, zsign_nat x (S (y +  x)) = (0,1).
  Proof.
    induction x.
    intro.
    simpl.
    reflexivity.
    intros.
    simpl.
    rewrite <- plus_n_Sm with (n:=y) (m:=x).
    apply IHx.
  Qed.

  Lemma calc_ASO: forall x y:nat, zsign_nat (S (y + x)) x = (1,0).
  Proof.
    induction x.
    intro.
    simpl.
    reflexivity.
    intro.
    simpl.
    rewrite <- plus_n_Sm with (n:= y) (m:= x). 
    apply IHx.    
  Qed.
  

  Lemma zsign_compat: forall (x y:Relative_integer), x =Z y -> zsign x = zsign y.
  Proof.
    assert (forall a b c d:nat, a+d=b+c -> zsign_nat a b = zsign_nat c d) as L.
    induction a.
    intros.
    induction b.
    rewrite plus_O_n in H.
    rewrite plus_O_n in H.
    rewrite H.
    rewrite calc_AOO.
    rewrite calc_AOO.
    reflexivity.
    rewrite plus_O_n in H.
    rewrite H.
    simpl.
    rewrite calc_AOS.
    reflexivity.
    induction b.
    intros.
    rewrite plus_O_n in H.
    rewrite plus_Sn_m in H.
    rewrite <- H.
    rewrite calc_ASO.
    simpl.
    reflexivity.
    intros.
    simpl.
    rewrite plus_Sn_m with (n:=a) (m:=d) in H.
    rewrite plus_Sn_m with (n:=b) (m:=c) in H.
    apply eq_add_S in H.
    apply IHa.
    assumption.
    intro.
    intro.
    unfold eqz.
    unfold zsign.
    intros.
    apply L.
    rewrite H.
    apply nsr_plus_commutative.
  Qed.

  Lemma cases_sign: forall x:Relative_integer,
      (x =Z O_Z) \/ (exists p:nat, x =Z (S p,0)) \/ (exists q:nat, x=Z (0,S q)).
  Proof.
    assert (forall a b:nat,
               a + 0 = 0 + b \/
               (exists c:nat, a + 0 = S c + b) \/
               (exists d:nat, a + S d = 0 + b)) as L.  
    induction a.
    induction b.
    left.
    simpl.
    reflexivity.
    simpl in IHb.
    destruct IHb.
    rewrite <- H.
    right.
    right.
    exists 0.
    reflexivity.
    right.
    right.
    exists b.
    reflexivity.
    induction b.
    right.
    left.
    exists a.
    reflexivity.
    destruct IHb.
    right.
    right.
    exists 0.
    rewrite <- plus_n_Sm with (n:=S a) (m:=0).
    rewrite <- plus_n_Sm with (n:=0) (m:=b).
    apply eq_S.
    assumption.
    destruct H.
    destruct H as (e,He).
    induction e.
    left.
    rewrite <- plus_n_Sm with (n:= 0) (m:=b).
    rewrite <- plus_Sn_m with (n:=0) (m:=b).
    assumption.
    right.
    left.
    exists e.
    rewrite <- plus_n_Sm with (n:= S e) (m:=b).
    rewrite <- plus_Sn_m with (n:=S e) (m:=b).
    assumption.
    right.
    right.
    destruct H as (f,Hf).
    exists (S f).
    rewrite <- plus_n_Sm with (n:= S a) (m:= S f).
    rewrite <- plus_n_Sm with (n:= 0) (m:= b).
    apply eq_S.
    assumption.
    intro.
    unfold eqz.
    simpl.
    simpl in L.
    apply L.
  Qed.

  Lemma zsign_zero: zsign O_Z = O_Z.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Lemma zsign_positive: forall n:nat, zsign (S n, 0) = (1,0).
  Proof.
    intros.
    unfold zsign.
    simpl.
    reflexivity.
  Qed.

  Lemma zsign_negative: forall n:nat, zsign (0, S n) = (0,1).
  Proof.
    intros.
    unfold zsign.
    simpl.
    reflexivity.
  Qed.

  Ltac zrac m n:= rewrite zsign_compat with (x:=m) (y:=n).
  Lemma zsign_morphism: forall x y:Relative_integer, (zsign (x *Z y)) = (zsign x) *Z (zsign y).
  Proof.
    intros.
    destruct cases_sign with (x:=x).  
    apply eq_trans with (y:= zsign (O_Z *Z y)).
    apply zsign_compat.
    apply Z_mult_compatibility.
    assumption.
    zer.  
    rewrite zsign_compat with (x:=x) (y:= O_Z).
    rewrite zsign_compat with (x:= O_Z *Z y) (y:= O_Z).
    rewrite zsign_zero.
    unfold Z_mult.
    simpl.
    reflexivity.
    zet (y *Z O_Z).
    zcom.
    apply Z_zero_product.
    assumption.
    destruct cases_sign with (x:=y).
    apply eq_trans with (y:= zsign (x *Z O_Z)).
    apply zsign_compat.
    apply Z_mult_compatibility.
    zer.
    assumption.
    rewrite zsign_compat with (x:=y) (y:= O_Z).
    rewrite zsign_compat with (x:= x *Z O_Z) (y:= O_Z).
    unfold Z_mult.
    simpl.
    mom (fst (zsign x)) 0.
    mom (snd (zsign x)) 0.
    simpl.
    rewrite zsign_zero.
    reflexivity.
    apply Z_zero_product.
    assumption.
    destruct H.
    destruct H as(p,Hp).
    destruct H0.
    destruct H as (q, Hq).
    zrac x (S p,0).
    zrac y (S q,0).
    zrac (x *Z y) ((S p, 0) *Z (S q, 0)).  
    unfold Z_mult.
    simpl.
    mom p 0.
    simpl.
    apply zsign_positive.
    apply Z_mult_compatibility.
    assumption.
    assumption.
    assumption.
    assumption.
    destruct H as (q, Hq).
    zrac x (S p,0).
    zrac y (0,S q).
    zrac (x *Z y) ((S p, 0) *Z (0, S q)).  
    unfold Z_mult.
    simpl.
    mom p 0.
    simpl.
    apply zsign_negative.
    apply Z_mult_compatibility.
    assumption.
    assumption.
    assumption.
    assumption.
    destruct H as(p,Hp).
    destruct H0.
    destruct H as (q, Hq).
    zrac x (0, S p).
    zrac y (S q,0).
    zrac (x *Z y) ((0, S p) *Z (S q, 0)).  
    unfold Z_mult.
    simpl.
    mom p 0.
    simpl.
    apply zsign_negative.
    apply Z_mult_compatibility.
    assumption.
    assumption.
    assumption.
    assumption.
    destruct H as (q, Hq).
    zrac x (0, S p).
    zrac y (0,S q).
    zrac (x *Z y) ((0, S p) *Z (0, S q)).  
    unfold Z_mult.
    simpl.
    mom p 0.
    simpl.
    apply zsign_positive.
    apply Z_mult_compatibility.
    assumption.
    assumption.
    assumption.
    assumption.
  Qed.
  
  Lemma zsign_involution: forall x:Relative_integer, zsign (zsign x) = (zsign x).
  Proof.
    intros.
    destruct cases_sign with (x:=x).
    zrac x O_Z.
    compute.
    reflexivity.
    assumption.
    destruct H.
    destruct H as (p,Hp).
    zrac x (S p,0).
    compute.
    reflexivity.
    assumption.
    destruct H as (q,Hq).
    zrac x (0,S q).
    compute.
    reflexivity.
    assumption.
  Qed.  

End Signs_of_relative_integers.
(* ****** BONUS ******  
In the section below, we build a counter-example to the following fallacy seen on a forum:
"the  distributivity of the product over the sum is equivalent to the sign rule"  
*)

Section bonus_signs.

  Let D_map (x y:Relative_integer):= zsign x *Z zsign y.

  Ltac zrac m n:= rewrite zsign_compat with (x:=m) (y:=n).
  
  Lemma D_associative: forall x y z:Relative_integer, D_map (D_map x y) z = D_map x (D_map y z).
  Proof.
    intros.
    unfold D_map.
    apply eq_trans with (y:= zsign (zsign x *Z zsign y) *Z (zsign (zsign z))).
    apply f_equal.
    apply eq_sym.
    apply zsign_involution.
    apply eq_trans with (y:= zsign ((zsign x *Z zsign y) *Z (zsign z))).
    apply eq_sym.
    apply zsign_morphism.
    apply eq_trans with (y:= zsign (zsign x) *Z (zsign (zsign y *Z zsign z))).
    apply eq_trans with (y:= zsign ((zsign x) *Z (zsign y *Z zsign z))).
    apply zsign_compat.
    zes.
    apply Z_mult_associative.
    apply zsign_morphism.
    rewrite zsign_involution with (x:=x).
    reflexivity.
  Qed.

  Lemma D_commutative: forall x y:Relative_integer, D_map x y = D_map y x.
  Proof.
    intros.
    unfold D_map.
    rewrite <- zsign_morphism.
    rewrite <- zsign_morphism.
    apply zsign_compat.
    zcom.
  Qed.

  Lemma D_zero: forall x:Relative_integer, D_map x O_Z = O_Z.
  Proof.
    intros.
    unfold D_map.
    rewrite <- zsign_morphism.
    zrac (x *Z O_Z) O_Z.
    apply zsign_zero.
    apply Z_zero_product.
  Qed.

  Lemma D_sign_rule: forall x y:Relative_integer, D_map x y = D_map (Z_opp x) (Z_opp y).
  Proof.
    intros.
    unfold D_map.
    rewrite <- zsign_morphism.
    rewrite <- zsign_morphism.
    apply zsign_compat.
    zes.
    apply sign_rule.
  Qed.

  Lemma D_compat:forall x x' y y':Relative_integer, ((x =Z x')/\(y =Z y'))-> D_map x y = D_map x' y'.
  Proof.
 intros.   
 unfold D_map.
 rewrite <- zsign_morphism.
 rewrite <- zsign_morphism.
 apply zsign_compat.
 apply Z_mult_compatibility.
 apply H.
 apply H.
  Qed.
       
  
  Theorem sign_counter_example: exists D: Relative_integer -> Relative_integer -> Relative_integer,
      (forall x x' y y':Relative_integer, ((x =Z x')/\(y =Z y'))-> D x y =Z D x' y')/\
      (forall x y:Relative_integer, D x y =Z D(Z_opp x) (Z_opp y)) /\
      (forall p q r:Relative_integer, D p (D q r) =Z D (D p q) r) /\
      (forall x y:Relative_integer, D x y =Z D y x) /\
      (forall x:Relative_integer, D x (0,0) =Z (0,0)) /\
      (~(D (I_Z +Z I_Z) I_Z) =Z (D I_Z I_Z) +Z (D I_Z I_Z)).
  Proof.
    assert (forall x y:Relative_integer, x = y -> x =Z y) as R.
    intros.
    rewrite H.
    zer.
    exists D_map.
    split.
    intros.
    apply R.
    unfold D_map.
    apply D_compat.
    assumption.
    split.
    intros.
    apply R.
    apply D_sign_rule.
    split.
    intros.
    apply R.
    apply eq_sym.
    apply D_associative.
    split.
    intros.
    apply R.
    apply D_commutative.
    split.
    intros.
    apply R.
    apply D_zero.
    compute.
    discriminate.
  Qed.
            
End bonus_signs.

Section nat_embedding.

  Definition n_to_z (x:nat):Relative_integer:= (x,0).

  Theorem n_to_z_injective: forall x y:nat, (n_to_z x) =Z (n_to_z y) -> x = y.
  Proof.
    intro.
    intro.
    unfold n_to_z.
    unfold eqz.
    simpl.
    com x 0.
    com y 0.
    simpl.
    intro.
    assumption.
  Qed.

  Theorem n_to_z_zero: n_to_z 0 =Z O_Z.
  Proof.
    unfold n_to_z.
    unfold eqz.
    simpl.
    reflexivity.
  Qed.

  Theorem n_to_z_one: n_to_z 1 =Z I_Z.
  Proof.
    unfold n_to_z.
    unfold eqz.
    simpl.
    reflexivity.
  Qed.

  Theorem n_to_z_sum: forall x y:nat, n_to_z (x + y) =Z (n_to_z x) +Z (n_to_z y).
  Proof.
    unfold n_to_z.
    unfold eqz.
    intros.
    simpl.
    reflexivity.
  Qed.

  Theorem n_to_z_product: forall x y:nat, n_to_z (x * y) =Z (n_to_z x) *Z (n_to_z y).
  Proof.
    unfold n_to_z.
    unfold eqz.
    intros.
    simpl.
    mom x 0.
    simpl.
    com (x * y + 0) 0.
    simpl.
    reflexivity.
  Qed.

  Theorem n_generates_z: forall x:Relative_integer, exists m n:nat, x +Z (n_to_z m) =Z (n_to_z n).
  Proof.
    intros.
    destruct x as (p,q).
    exists q.
    exists p.
    unfold n_to_z.
    unfold eqz.
    simpl.
    alr p q 0.
    reflexivity.
  Qed.
  (*The above theorem states that every relative integer is the difference of two natural 
    integers.*)
  
End nat_embedding.
(*   
(*Uncomment this part if you want to use the ring library, declare nat as a semi ring
and Relative_integer as a ring and incorporate rings tactics *)

Require Import Ring.

Theorem nat_semi_ring: @semi_ring_theory nat 0 1 plus mult eq.
Proof.
  split.
  apply nsr_O_plus_neutral.
  apply nsr_plus_commutative.
  apply nsr_plus_associative.
  apply nsr_I_mult_neutral.
  apply nsr_O_absorbs.
  apply nsr_mult_commutative.
  apply nsr_mult_associative.
  apply nsr_right_distributivity.
Qed.

Add Ring the_set_of_natural_integers_is_a_semi_ring: nat_semi_ring.

  
Require Import Setoid.

Lemma equiv_eqz: Equivalence eqz.
Proof.
  split.
  unfold Reflexive.
  apply eqz_reflexive.
  unfold Symmetric.    
  apply eqz_symmetric.
  unfold Transitive.
  apply eqz_transitive.
Qed.

Theorem Z_ring: @ring_theory Relative_integer O_Z I_Z Z_plus Z_mult Z_minus Z_opp eqz.
Proof.
  split.
  apply Z_zero_plus_neutral.
  apply Z_plus_commutative.
  apply Z_plus_associative.
  apply Z_un_neutral.
  apply Z_mult_commutative.
  apply Z_mult_associative.
  apply Z_right_distributivity.
  apply Z_minus_opp.
  apply Z_opp_group.
Qed.

Lemma Z_compatibility: ring_eq_ext  Z_plus Z_mult Z_opp eqz.
Proof.
  unfold Morphisms.Proper.
  unfold Morphisms.respectful.
  split.
  unfold Morphisms.Proper.
  unfold Morphisms.respectful.
  intro.
  intro.
  intros.
  apply Z_sum_compatibility.
  assumption.
  assumption.  
  unfold Morphisms.Proper.
  unfold Morphisms.respectful.
  intros.
  apply Z_mult_compatibility.
  assumption.
  assumption.
  unfold Morphisms.Proper.
  unfold Morphisms.respectful.
  apply Z_opp_compatibility.
Qed.
*)