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.