X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Farithmetics%2FZ.ma;h=1904f684932789508909c270f88747a801f8b1b5;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=9045a6d8ad5ce4c10731570c92b4b4a535524d84;hpb=6b229b2d85552d78fcbce805248f87559f7f6df8;p=helm.git

diff --git a/helm/software/matita/nlibrary/arithmetics/Z.ma b/helm/software/matita/nlibrary/arithmetics/Z.ma
index 9045a6d8a..1904f6849 100644
--- a/helm/software/matita/nlibrary/arithmetics/Z.ma
+++ b/helm/software/matita/nlibrary/arithmetics/Z.ma
@@ -346,6 +346,8 @@ ncut
 ##|#Hcut;napply Hcut;napply eqZb_to_Prop]
 nqed.
 
+include "arithmetics/compare.ma".
+
 ndefinition Z_compare : Z → Z → compare ≝
 λx,y:Z.
   match x with
@@ -508,7 +510,7 @@ ntheorem Zplus_Zsucc_Zpred: ∀x,y. x+y = (Zsucc x)+(Zpred y).
    ##[//
    ##|#n;nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite > (Zsucc_Zpred ?);//
    ##|//]
-##|ncases y;//
+##|ncases y;/2/;
 ##|ncases y
    ##[#n;nrewrite < (sym_Zplus ??);nrewrite < (sym_Zplus (Zpred OZ) ?);
       nrewrite < (Zpred_Zplus_neg_O ?);nrewrite > (Zpred_Zsucc ?);//