(* *)
(**************************************************************************)
-set "baseuri" "cic:/matita/Z/orders".
-
include "Z/z.ma".
include "nat/orders.ma".
| (pos m) \Rightarrow True
| (neg m) \Rightarrow m \leq n ]].
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer 'less or equal to'" 'leq x y = (cic:/matita/Z/orders/Zle.con x y).
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer 'neither less nor equal to'" 'nleq x y =
- (cic:/matita/logic/connectives/Not.con (cic:/matita/Z/orders/Zle.con x y)).
+interpretation "integer 'less or equal to'" 'leq x y = (Zle x y).
+interpretation "integer 'neither less nor equal to'" 'nleq x y = (Not (Zle x y)).
definition Zlt : Z \to Z \to Prop \def
\lambda x,y:Z.
| (pos m) \Rightarrow True
| (neg m) \Rightarrow m<n ]].
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer 'less than'" 'lt x y = (cic:/matita/Z/orders/Zlt.con x y).
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "integer 'not less than'" 'nless x y =
- (cic:/matita/logic/connectives/Not.con (cic:/matita/Z/orders/Zlt.con x y)).
+interpretation "integer 'less than'" 'lt x y = (Zlt x y).
+interpretation "integer 'not less than'" 'nless x y = (Not (Zlt x y)).
theorem irreflexive_Zlt: irreflexive Z Zlt.
unfold irreflexive.unfold Not.