(*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)).
definition Zlt : Z \to Z \to Prop \def
\lambda x,y:Z.
(*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)).
theorem irreflexive_Zlt: irreflexive Z Zlt.
change with \forall x:Z. x < x \to False.