set "baseuri" "cic:/matita/CoRN-Decl/model/structures/Zsec".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: Zsec.v,v 1.5 2004/04/06 15:46:05 lcf Exp $ *)
inline "cic:/CoRN/model/structures/Zsec/ap_Z.con".
+(* NOTATION
+Infix "{#Z}" := ap_Z (no associativity, at level 90).
+*)
+
(*#* Some properties of apartness:
*)
(* begin hide *)
-coercion "cic:/matita/CoRN-Decl/model/structures/Zsec/Zpos.con" 0 (* compounds *).
+coercion cic:/Coq/ZArith/BinInt/Z.ind#xpointer(1/1/2) 0 (* compounds *).
(* end hide *)