feat(data/{nat,int}/parity): the 'even' predicate on nat and int

[avigad]

The predicate even is defined in terms of exists so that we can use cases to extract the half. The theorem even_iff shows that even n is equivalent to n % 2 = 0.

As the examples at the end of each file show, simp will reduce concrete instances to true or false, and simp with parity_simps will solve harder problems.

Note: @digama0 used to be against introducing a definition for even, but now is in favor.

[cipher1024]

What used to be the argument and what made @digama0 change his mind?

[digama0]

The argument was to prefer 2 | x and not (2 | x) for even and odd. But we want to have a theory of parity regardless, and even has been reinvented many times by users of mathlib. The easiest way to forestall this is to define it in mathlib so that people find it when they need it.