X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Forders.ma;h=8255787f98988252369855dca4f5e075de451f2d;hb=4dc47c9675ffd5fa50296ffaa9b5997501518c98;hp=6336a5e9bf12bec1e9ddca458d5d98b36d1e548a;hpb=c445ba5534cccde19016c92660ab52777af221c0;p=helm.git

diff --git a/helm/software/matita/library/nat/orders.ma b/helm/software/matita/library/nat/orders.ma
index 6336a5e9b..8255787f9 100644
--- a/helm/software/matita/library/nat/orders.ma
+++ b/helm/software/matita/library/nat/orders.ma
@@ -20,32 +20,28 @@ inductive le (n:nat) : nat \to Prop \def
   | le_n : le n n
   | le_S : \forall m:nat. le n m \to le n (S m).
 
-interpretation "natural 'less or equal to'" 'leq x y = (cic:/matita/nat/orders/le.ind#xpointer(1/1) x y).
+interpretation "natural 'less or equal to'" 'leq x y = (le x y).
 
-interpretation "natural 'neither less nor equal to'" 'nleq x y =
-  (cic:/matita/logic/connectives/Not.con
-    (cic:/matita/nat/orders/le.ind#xpointer(1/1) x y)).
+interpretation "natural 'neither less nor equal to'" 'nleq x y = (Not (le x y)).
 
 definition lt: nat \to nat \to Prop \def
 \lambda n,m:nat.(S n) \leq m.
 
-interpretation "natural 'less than'" 'lt x y = (cic:/matita/nat/orders/lt.con x y).
+interpretation "natural 'less than'" 'lt x y = (lt x y).
 
-interpretation "natural 'not less than'" 'nless x y =
-  (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/orders/lt.con x y)).
+interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)).
 
 definition ge: nat \to nat \to Prop \def
 \lambda n,m:nat.m \leq n.
 
-interpretation "natural 'greater or equal to'" 'geq x y = (cic:/matita/nat/orders/ge.con x y).
+interpretation "natural 'greater or equal to'" 'geq x y = (ge x y).
 
 definition gt: nat \to nat \to Prop \def
 \lambda n,m:nat.m<n.
 
-interpretation "natural 'greater than'" 'gt x y = (cic:/matita/nat/orders/gt.con x y).
+interpretation "natural 'greater than'" 'gt x y = (gt x y).
 
-interpretation "natural 'not greater than'" 'ngtr x y =
-  (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/orders/gt.con x y)).
+interpretation "natural 'not greater than'" 'ngtr x y = (Not (gt x y)).
 
 theorem transitive_le : transitive nat le.
 unfold transitive.intros.elim H1.
@@ -154,9 +150,7 @@ elim n;
 [ simplify;
   apply le_O_n
 | simplify;
-  generalize in match H1;
-  clear H1;
-  elim m;
+  elim m in H1 ⊢ %;
   [ elim (not_le_Sn_O ? H1)
   | simplify;
     apply le_S_S_to_le;