After axiomatising the natural numbers again and proving theorems in them, I turn my attention to the integers.

Garavel (2017) talks about axiomatisations of the integers, noting that there is no common standard. I am implementing the “two sorts and two free constructors” approach mentioned in that paper, which is considered the best candidate for a standard axiomatisation. (Coq’s standard library uses two sorts and three free constructors.) If `n`

is a natural number, `pos n`

represents the nonnegative `n`

and `neg n`

represents the negative `-n-1`

.

```
Inductive int: Type:=
| pos (n: nat)
| neg (n: nat).
Fixpoint p1 n:= match n with
| pos k => pos (S k)
| neg 0 => pos 0
| neg (S k) => neg k end.
Fixpoint m1 n:= match n with
| pos (S k) => pos k
| pos 0 => neg 0
| neg k => neg (S k) end.
Fixpoint minus n:= match n with
| pos (S k) => neg k
| pos 0 => pos 0
| neg k => pos (S k) end.
Theorem minus_involutive: forall n, minus (minus n) = n.
Proof. intros. do 2 destruct n. all: auto. Qed.
Fixpoint add m n {struct n}:= match n with
| pos 0 => m
| neg 0 => m1 m
| pos (S k) => add (p1 m) (pos k)
| neg (S k) => add (m1 m) (neg k) end.
```

But when I try to define addition using the last code block above, I get an error saying that the definition is ill-formed, even though it is plain to see that the fix is decreasing on the second argument. How can I remedy this?