feat(data/nat/prime): add coprime_of_prime lemmas (#10534)
feat(data/nat/prime): add coprime_of_prime lemmas (#10534)


Adds `coprime_of_lt_prime` and `eq_or_coprime_of_le_prime`, which help one to prove a number is coprime to a prime. Spun off of #9080.





leanprover-community/mathlib,leanprover-community/mathlib