In the last post, I showed how to prove, using only elementary tools, that zero is not the successor of any natural number, that `O = succ(m)`

leads to a contradiction.

In this post, we’ll see that the successor function is injective. Writing `S`

in place of `succ`

, we’ll show that if `S(m) = S(n)`

, then `m = n`

.

As before, we start with our own version of the natural numbers.

```
inductive mynat : Type
| O : mynat
| S : mynat → mynat
```

The strategy for our proof will be to find a predicate `P`

on pairs of natural numbers such that on the assumption `h : S(m) = S(n)`

, the following criteria are satisfied:

- From
`h₃`

, a proof of`P (S m) (S n)`

, we can easily prove the result`m = n`

. - We can easily construct
`h₁`

, a proof of`S(m) = S(m) → P (S m) (S m)`

.

Why does this help? Substituting equation `h`

into `h₁`

gives

`h₂ : S(m) = S(n) → P (S m) (S n)`

. But we know `h`

, a proof of the antecedent of this implication, and hence we derive `h₃ := h₂ h`

, the desired proof of `P (S m) (S n)`

. From this, we prove our initial target `m = n`

.

I’m sure you will agree that the first condition above is satisfied if `P`

is chosen so that `P (S m) (S n) = m = n`

.

Since this is a good candidate for `P`

, we’ll give it a Lean definition.

```
def P : mynat → mynat → Prop
| (S a) (S b) := a = b
| _ _ := true
```

The second pattern in the definition isn’t used on our proof, but Lean functions are total, so we must define `P`

in all cases.

What remains is to prove the second criterion. By definition, `P (S m) (S m)`

is simply `m = m`

. This is true by reflexivity.

Those are all the ingredients. Time to assemble them up into a Lean proof.

```
lemma succ_inj (m n : mynat) (h : S m = S n) : m = n :=
have h₁ : S(m) = S(m) → P (S m) (S m), from λ _, rfl,
have h₂ : S(m) = S(n) → P (S m) (S n), from h ▸ h₁,
have h₃ : P (S m) (S n), from h₂ h,
show m = n, from h₃
```