X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Forders.ma;h=811706867e4729f52f57ffd1d7f9183073c122f2;hb=78044035b4419e569df0d7f6a7f96fa32d21a19d;hp=d592ed0afa4951d6d080109771eab40923568984;hpb=da83446deba30fbe32b9bf617d83bd22cc9c9770;p=helm.git

diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma
index d592ed0af..811706867 100644
--- a/helm/matita/library/nat/orders.ma
+++ b/helm/matita/library/nat/orders.ma
@@ -24,12 +24,19 @@ inductive le (n:nat) : nat \to Prop \def
 
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural 'less or equal to'" 'leq x y = (cic:/matita/nat/orders/le.ind#xpointer(1/1) x y).
+(*CSC: the URI must disappear: there is a bug now *)
+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)).
 
 definition lt: nat \to nat \to Prop \def
 \lambda n,m:nat.(S n) \leq m.
 
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural 'less than'" 'lt x y = (cic:/matita/nat/orders/lt.con x y).
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "natural 'not less than'" 'nless x y =
+  (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/orders/lt.con x y)).
 
 definition ge: nat \to nat \to Prop \def
 \lambda n,m:nat.m \leq n.
@@ -42,6 +49,9 @@ definition gt: nat \to nat \to Prop \def
 
 (*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural 'greater than'" 'gt x y = (cic:/matita/nat/orders/gt.con x y).
+(*CSC: the URI must disappear: there is a bug now *)
+interpretation "natural 'not greater than'" 'ngtr x y =
+  (cic:/matita/logic/connectives/Not.con (cic:/matita/nat/orders/gt.con x y)).
 
 theorem transitive_le : transitive nat le.
 simplify.intros.elim H1.