-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural 'less or equal to'" 'leq x y = (cic:/matita/library_autobatch/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/library_autobatch/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 = (Not (le x y)).