added notation for nleq, nlgt, ...

[helm.git] / helm / matita / library / nat / orders.ma

diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma
index d592ed0afa4951d6d080109771eab40923568984..811706867e4729f52f57ffd1d7f9183073c122f2 100644 (file)
--- 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.