Committing all the recent development of Andrea after the merge between his

[helm.git] / helm / matita / library / Z / z.ma

diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma
index d3bc2ee2584529c00802746e4e5e792ea0c4242e..cdc0e44d7c28f29fb01681a6d2b52a139a2955d0 100644 (file)
--- a/helm/matita/library/Z/z.ma
+++ b/helm/matita/library/Z/z.ma
@@ -108,7 +108,7 @@ definition Zplus :Z \to Z \to Z \def
     | (pos m) \Rightarrow
         match y with
          [ OZ \Rightarrow x
-         | (pos n) \Rightarrow (pos (S (m+n)))
+         | (pos n) \Rightarrow (pos (pred ((S m)+(S n))))
          | (neg n) \Rightarrow 
               match nat_compare m n with
                 [ LT \Rightarrow (neg (pred (n-m)))
@@ -122,7 +122,7 @@ definition Zplus :Z \to Z \to Z \def
                 [ LT \Rightarrow (pos (pred (n-m)))
                 | EQ \Rightarrow OZ
                 | GT \Rightarrow (neg (pred (m-n)))]     
-         | (neg n) \Rightarrow (neg (S (m+n)))]].
+         | (neg n) \Rightarrow (neg (pred ((S m)+(S n))))]].
 
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "integer plus" 'plus x y = (cic:/matita/Z/z/Zplus.con x y).
@@ -140,7 +140,7 @@ theorem sym_Zplus : \forall x,y:Z. x+y = y+x.
 intros.elim x.rewrite > Zplus_z_OZ.reflexivity.
 elim y.simplify.reflexivity.
 simplify.
-rewrite < sym_plus.reflexivity.
+rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity.
 simplify.
 rewrite > nat_compare_n_m_m_n.
 simplify.elim nat_compare ? ?.simplify.reflexivity.
@@ -151,7 +151,7 @@ simplify.rewrite > nat_compare_n_m_m_n.
 simplify.elim nat_compare ? ?.simplify.reflexivity.
 simplify. reflexivity.
 simplify. reflexivity.
-simplify.rewrite < sym_plus.reflexivity.
+simplify.rewrite < plus_n_Sm. rewrite < plus_n_Sm.rewrite < sym_plus.reflexivity.
 qed.
 
 theorem Zpred_Zplus_neg_O : \forall z:Z. Zpred z = (neg O)+z.
@@ -177,9 +177,9 @@ elim n.elim m.
 simplify.reflexivity.
 simplify.reflexivity.
 elim m.
-simplify.
+simplify.rewrite < plus_n_Sm.
 rewrite < plus_n_O.reflexivity.
-simplify.
+simplify.rewrite < plus_n_Sm.
 rewrite < plus_n_Sm.reflexivity.
 qed.
 
@@ -206,7 +206,7 @@ elim n.elim m.
 simplify.reflexivity.
 simplify.reflexivity.
 elim m.
-simplify.rewrite < plus_n_Sm.reflexivity.
+simplify.rewrite > plus_n_Sm.reflexivity.
 simplify.rewrite > plus_n_Sm.reflexivity.
 qed.