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 *)