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

diff --git a/helm/software/matita/nlibrary/arithmetics/Z.ma b/helm/software/matita/nlibrary/arithmetics/Z.ma
index 7a0f7f080..1904f6849 100644
--- a/helm/software/matita/nlibrary/arithmetics/Z.ma
+++ b/helm/software/matita/nlibrary/arithmetics/Z.ma
@@ -55,7 +55,7 @@ ntheorem OZ_test_to_Prop : ∀z:Z.
   |false ⇒ z ≠ OZ].
 #z;ncases z
 ##[napply refl
-##|##*:#z1;#H;ndestruct]
+##|##*:#z1;napply nmk;#H;ndestruct]
 nqed.
 
 (* discrimination *)
@@ -74,34 +74,37 @@ nqed.
 \def injective_neg. *)
 
 ntheorem not_eq_OZ_pos: ∀n:nat. OZ ≠ pos n.
-#n;#H;ndestruct;
+#n;napply nmk;#H;ndestruct;
 nqed.
 
 ntheorem not_eq_OZ_neg :∀n:nat. OZ ≠ neg n.
-#n;#H;ndestruct;
+#n;napply nmk;#H;ndestruct;
 nqed.
 
 ntheorem not_eq_pos_neg : ∀n,m:nat. pos n ≠ neg m.
-#n;#m;#H;ndestruct;
+#n;#m;napply nmk;#H;ndestruct;
 nqed.
 
 ntheorem decidable_eq_Z : ∀x,y:Z. decidable (x=y).
 #x;#y;ncases x;
 ##[ncases y;
    ##[@;//
-   ##|##*:#n;@2;#H;ndestruct]
+   ##|##*:#n;@2;napply nmk;#H;ndestruct]
 ##|#n;ncases y;
-   ##[@2;#H;ndestruct;
+   ##[@2;napply nmk;#H;ndestruct;
    ##|#m;ncases (decidable_eq_nat n m);#H;
       ##[nrewrite > H;@;//
-      ##|@2;#H2;napply H;ndestruct;//]
-   ##|#m;@2;#H;ndestruct]
+      ##|@2;napply nmk;#H2;nelim H;
+         (* bug if you don't introduce H3 *)#H3;ndestruct;
+         napply H3;@]
+   ##|#m;@2;napply nmk;#H;ndestruct]
 ##|#n;ncases y;
-   ##[@2;#H;ndestruct;
-   ##|#m;@2;#H;ndestruct
+   ##[@2;napply nmk;#H;ndestruct;
+   ##|#m;@2;napply nmk;#H;ndestruct
    ##|#m;ncases (decidable_eq_nat n m);#H;
       ##[nrewrite > H;@;//
-      ##|@2;#H2;napply H;ndestruct;//]##]##]
+      ##|@2;napply nmk;#H2;nelim H;#H3;ndestruct;
+         napply H3;@]##]##]
 nqed.
 
 ndefinition Zsucc ≝
@@ -180,7 +183,7 @@ interpretation "integer 'not less than'" 'nless x y = (Not (Zlt x y)).
 
 ntheorem irreflexive_Zlt: irreflexive Z Zlt.
 #x;ncases x
-##[//
+##[napply nmk;//
 ##|##*:#n;napply (not_le_Sn_n n) (* XXX: auto?? *)]
 nqed.
 
@@ -276,7 +279,7 @@ ntheorem Zlt_to_Zle: ∀x,y:Z. x < y → Zsucc x ≤ y.
 ##|#n;ncases y
    ##[##1,2:ncases n;//
    ##|#p;ncases n;nnormalize;
-      ##[napply not_le_Sn_O (* XXX: auto? *)
+      ##[#H;nelim (not_le_Sn_O p);#H2;napply H2;//; (* XXX: auto? *)
       ##|#m;napply le_S_S_to_le (* XXX: auto? *)]
    ##]
 ##]
@@ -315,17 +318,17 @@ ntheorem eqZb_to_Prop:
    ##|napply not_eq_OZ_pos (* XXX: auto? *)
    ##|napply not_eq_OZ_neg (* XXX: auto? *)]
 ##|#n;ncases y;
-   ##[#H;napply not_eq_OZ_pos;//;
+   ##[napply nmk;#H;nelim (not_eq_OZ_pos n);#H2;/2/;
    ##|#m;napply eqb_elim;
       ##[//
-      ##|#H;#H2;napply H;ndestruct;//]
+      ##|#H;napply nmk;#H2;nelim H;#H3;ndestruct;/2/]
    ##|#m;napply not_eq_pos_neg]
 ##|#n;ncases y
-   ##[#H;napply not_eq_OZ_neg;//;
-   ##|#m;#H;ndestruct
+   ##[napply nmk;#H;nelim (not_eq_OZ_neg n);#H;/2/;
+   ##|#m;napply nmk;#H;ndestruct
    ##|#m;napply eqb_elim;
       ##[//
-      ##|#H;#H2;napply H;ndestruct;//]
+      ##|#H;napply nmk;#H2;ndestruct;nelim H;/2/]
    ##]
 ##]
 nqed.
@@ -343,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
@@ -505,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 ?);//