X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2FZ%2Forders.ma;h=94aa9416c68d3ffd26596f84d0576d1ba3e34e00;hb=5a702cea95883f7095c16b450e065ccb1714fc5a;hp=ec1d6fb525f8a270f6058ebfba7f13118ee44fc9;hpb=cd4e16d545b0ca42c37e2f79f63e6c25c6ad4480;p=helm.git

diff --git a/helm/matita/library/Z/orders.ma b/helm/matita/library/Z/orders.ma
index ec1d6fb52..94aa9416c 100644
--- a/helm/matita/library/Z/orders.ma
+++ b/helm/matita/library/Z/orders.ma
@@ -38,6 +38,9 @@ definition Zle : Z \to Z \to Prop \def
 
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "integer 'less or equal to'" 'leq x y = (cic:/matita/Z/orders/Zle.con x y).
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "integer 'neither less nor equal to'" 'nleq x y =
+  (cic:/matita/logic/connectives/Not.con (cic:/matita/Z/orders/Zle.con x y)).
 
 definition Zlt : Z \to Z \to Prop \def
 \lambda x,y:Z.
@@ -60,6 +63,9 @@ definition Zlt : Z \to Z \to Prop \def
     
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "integer 'less than'" 'lt x y = (cic:/matita/Z/orders/Zlt.con x y).
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "integer 'not less than'" 'nless x y =
+  (cic:/matita/logic/connectives/Not.con (cic:/matita/Z/orders/Zlt.con x y)).
 
 theorem irreflexive_Zlt: irreflexive Z Zlt.
 change with \forall x:Z. x < x \to False.
@@ -94,23 +100,31 @@ simplify.apply H.
 qed.
 
 theorem Zlt_to_Zle: \forall x,y:Z. x < y \to Zsucc x \leq y.
-intros 2.elim x.
-cut OZ < y \to Zsucc OZ \leq y.
-apply Hcut. assumption.simplify.elim y.
-simplify.exact H1.
-simplify.exact H1.
-simplify.apply le_O_n.
-cut neg n < y \to Zsucc (neg n) \leq y.
-apply Hcut. assumption.elim n.
-cut neg O < y \to Zsucc (neg O) \leq y.
-apply Hcut. assumption.simplify.elim y.
-simplify.exact I.simplify.apply not_le_Sn_O n1 H2.
-simplify.exact I.
-cut neg (S n1) < y \to (Zsucc (neg (S n1))) \leq y.
-apply Hcut. assumption.simplify.
-elim y.
-simplify.exact I.
-simplify.apply le_S_S_to_le n2 n1 H3.
-simplify.exact I.
-exact H.
+intros 2.
+elim x.
+(* goal: x=OZ *)
+  cut OZ < y \to Zsucc OZ \leq y.
+    apply Hcut. assumption.
+    simplify.elim y. 
+      simplify.exact H1.
+      simplify.apply le_O_n.
+      simplify.exact H1.
+(* goal: x=pos *)      
+  exact H.
+(* goal: x=neg *)      
+  cut neg n < y \to Zsucc (neg n) \leq y.
+    apply Hcut. assumption.
+    elim n.
+      cut neg O < y \to Zsucc (neg O) \leq y.
+        apply Hcut. assumption.
+        simplify.elim y.
+          simplify.exact I.
+          simplify.exact I.
+          simplify.apply not_le_Sn_O n1 H2.
+      cut neg (S n1) < y \to (Zsucc (neg (S n1))) \leq y.
+        apply Hcut. assumption.simplify.
+        elim y.
+          simplify.exact I.
+          simplify.exact I.
+          simplify.apply le_S_S_to_le n2 n1 H3.
 qed.