Exercise 4.6.4 doesn't contain definition of `even`

[martincmartin]

In the exercises at the end of chapter 4, exercise 4 starts with:

import data.nat.basic

#check even

However, the check fails since even isn't defined.

is_even is defined earlier in the chapter as:

def is_even (a : nat) := ∃ b, a = 2 * b