X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2FZ%2Forders.ma;h=c39f693085398eedf4a95a9f15898f05e6cee264;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=94aa9416c68d3ffd26596f84d0576d1ba3e34e00;hpb=78044035b4419e569df0d7f6a7f96fa32d21a19d;p=helm.git

diff --git a/helm/matita/library/Z/orders.ma b/helm/matita/library/Z/orders.ma
index 94aa9416c..c39f69308 100644
--- a/helm/matita/library/Z/orders.ma
+++ b/helm/matita/library/Z/orders.ma
@@ -68,12 +68,12 @@ 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.
+change with (\forall x:Z. x < x \to False).
 intro.elim x.exact H.
-cut neg n < neg n \to False.
-apply Hcut.apply H.simplify.apply not_le_Sn_n.
-cut pos n < pos n \to False.
-apply Hcut.apply H.simplify.apply not_le_Sn_n.
+cut (neg n < neg n \to False).
+apply Hcut.apply H.simplify.unfold lt.apply not_le_Sn_n.
+cut (pos n < pos n \to False).
+apply Hcut.apply H.simplify.unfold lt.apply not_le_Sn_n.
 qed.
 
 theorem irrefl_Zlt: irreflexive Z Zlt
@@ -103,7 +103,7 @@ theorem Zlt_to_Zle: \forall x,y:Z. x < y \to Zsucc x \leq y.
 intros 2.
 elim x.
 (* goal: x=OZ *)
-  cut OZ < y \to Zsucc OZ \leq y.
+  cut (OZ < y \to Zsucc OZ \leq y).
     apply Hcut. assumption.
     simplify.elim y. 
       simplify.exact H1.
@@ -112,19 +112,19 @@ elim x.
 (* goal: x=pos *)      
   exact H.
 (* goal: x=neg *)      
-  cut neg n < y \to Zsucc (neg n) \leq y.
+  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.
+      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.
+          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.
+          simplify.apply (le_S_S_to_le n2 n1 H3).
 qed.