In Section 6.7 Induction Pitfalls there's a typo in:
To solve this issue, we need to replace 2 * n + 1 by a variable m and add an equation m = 2 * n + 1 as a hypothesis:
m : 2 * n + 1, hev : Even m ⊢ False
The goal should instead be:
m : ℕ, hm : m = 2 * n + 1, hev : Even m ⊢ False
This change is then also consistent with the goals shown immediately afterwards.
In Section 6.7 Induction Pitfalls there's a typo in:
The goal should instead be:
This change is then also consistent with the goals shown immediately afterwards.