update in groud_2 and models

[helm.git] / helm / software / matita / nlibrary / arithmetics / Z.ma

diff --git a/helm/software/matita/nlibrary/arithmetics/Z.ma b/helm/software/matita/nlibrary/arithmetics/Z.ma
index 9045a6d8ad5ce4c10731570c92b4b4a535524d84..1904f684932789508909c270f88747a801f8b1b5 100644 (file)
--- 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 ?);//