More notation (up to where the open bugs allow me to put it without adding

[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 5389418b5237d7bde8cf4a9424bba777a5b38a62..d269e5fe1b83485fc20203ef08c5e3e6d7c988aa 100644 (file)
--- a/helm/matita/library/nat/orders.ma
+++ b/helm/matita/library/nat/orders.ma
@@ -22,22 +22,25 @@ 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).
 
+(*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).
-alias symbol "leq" (instance 0) = "natural 'less or equal to'".
 
 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).
 
 definition ge: nat \to nat \to Prop \def
 \lambda n,m:nat.m \leq n.
 
+(*CSC: the URI must disappear: there is a bug now *)
 interpretation "natural 'greater or equal to'" 'geq x y = (cic:/matita/nat/orders/ge.con x y).
 
 definition gt: nat \to nat \to Prop \def
 \lambda n,m:nat.m<n.
 
+(*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).
 
 theorem transitive_le : transitive nat le.