Proof of Euclid's Lemma in N that does not use GCD I am looking for a proof of Euclid's Lemma, i.e if a prime number divides a product of two numbers then it must at least divide one of them.
I am coding this proof in Coq, and i'm doing it over natural numbers. I aim to prove the uniqueness of prime factorization (So I cannot use this lemma!). However, I can use the existence of a prime factorization, which I already proved.
I do not want to use the gcd algorithm as that would involve coding it in Coq and proving it is correct which may be difficult. The idea is to use this proof in a computer science course, so I do not want to overcomplicate things.
Is there any proof of this lemma that does not use gcd, or Bezout's lemma, or the uniqueness of prime factorization? Maybe something using induction?
Thank you in advance.
EDIT: The Proof should be on NATURAL NUMBERS. No answer did the proof in N.

The OP's stated goal is to prove the uniqueness of prime factorization using elementary/foundational techniques, perhaps by proving Euclid's lemma in a different way.
Since the end goal is to prove uniqueness in the FTA, of interest here are two similar elementary proofs.
(1) The wikipedia article: Elementary proof of uniqueness
which uses the distributivity law a couple of times.
(2) Bill Dubuque's: Elementary proof of the FTA
The 'hook' used there: every $n \gt 1$ has a least (unique) factor $p \ne 1$. The argument works around that to get the FTA. 
I think that the techniques found in the above arguments are beautiful, although those who have not invested the time most likely would not agree.
In conclusion, a budding $\text{AI MATH BOT}$ might enjoy chewing on this elementary theory!
