3
fun f : nat -> Z => (f 0%nat + 0)%Z
5
fun x : positive => Zpos x~0
7
fun x : positive => (Zpos x + 1)%Z
9
fun x : positive => Zpos x
11
fun x : positive => Zneg x~0
13
fun x : positive => (Zpos x~0 + 0)%Z
15
fun x : positive => (- Zpos x~0)%Z
17
fun x : positive => (- Zpos x~0 + 0)%Z
21
(0 + Z_of_nat (0 + 0))%Z