feat(data/nat/prime): add the subtype of prime numbers

[jcommelin]

Inspired by the perfectoid project.

[semorrison]

Nothing more to say about these? This might be slicing the salami a little thin. :-)

[digama0]

Why not define a set instead, and use set_coe?

[jcommelin]

Nope, we don't do anything with prime numbers. They only show up in the top-level file of the project...
We could just leave this definition in the project... I don't really care.

[NeilStrickland]

I have also added this type in #1073 (which contains lots of other things). I called it nat.primes. I think that it is probably better to have it in the nat namespace. Beyond that, I am not sure what is the best naming convention. Perhaps we should rename nat.prime to nat.is_prime and then the type can be called nat.prime.