+let rec pos2nat x \def
+ match x with
+ [ one \Rightarrow (S O)
+ | (next z) \Rightarrow S (pos2nat z)].
+
+let rec nat2int x \def
+ match x with
+ [ O \Rightarrow positive O
+ | (S z) \Rightarrow positive (S z)].
+
+coercion pos2nat.
+
+coercion nat2int.
+
+let rec plus x y \def
+ match x with
+ [ (positive n) \Rightarrow x
+ | (negative z) \Rightarrow y].
+
+theorem a: plus O one.