refactor(data/nat/prime): cleanup exists_infinite_primes (#271)
refactor(data/nat/prime): cleanup exists_infinite_primes (#271)

* removing unnecessary initial step
* giving names to ambiguous copies of `this`

leanprover-community/mathlib,leanprover-community/mathlib