Proof of Euclid's Lemma in N that does not use GCD

Question

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.

Answer 1

Claim 2 below should answer the question.

Since the only unit in $\mathbb{N}$ is $1$, we have

$p$ is prime iff $p\mid ab\implies p\mid a\lor p\mid b$

$p$ is irreducible iff $a\mid p\implies a=1\lor a=p$

Claim 1: $p$ is prime $\implies$ $p$ is irreducible

Proof: Assume that $a\mid p$. For some $b$, we have $$ p=ab\tag{1} $$ Since $p\mid ab$, we know that $p\mid a$ or $p\mid b$.

Case $p\mid a$: for some $c$, we have $a=pc$. Therefore, $(1)$ implies that $abc=a$. Since the only unit in $\mathbb{N}$ is $1$, we have that $b=c=1$. Therefore $a=p$.

Case $p\mid b$: for some $c$, we have $b=pc$. Therefore, $(1)$ implies that $abc = b$. Since the only unit in $\mathbb{N}$ is $1$, we have that $a=c=1$. Therefore, $a=1$.

Thus, assuming that $p$ is prime and $a\mid p$, we have shown that $a=1$ or $a=p$.

QED

Claim 2: $p$ is irreducible $\implies$ $p$ is prime

Proof: Assume that $p$ is irreducible, $p\mid ab$, and $p\nmid a$. Let $g$ be the smallest positive element of the set $$ S=\{\,ax+py:x,y\in\mathbb{Z}\,\}\tag{2} $$ If $g\nmid p$, then there is an $r$ so that $0\lt r\lt g$ and $qg+r=p$. However, then $$ r=p-q(ax+py)=a(-qx)+p(1-qy)\in S\tag{3} $$ but $g$ is the smallest positive element of $S$. Therefore, $g\mid p$. Similarly, $g\mid a$.

Since $p$ is irreducible, $g=1$ or $g=p$. Since $p\nmid a$ and $g\mid a$, we must have $g=1$. Therefore, we have $x,y$ so that $$ 1=ax+py\tag{4} $$ Since $p\mid ab$, for some $c$, we have $ab=pc$. Multiply $(4)$ by $b$ to get $$ \begin{align} b &=abx+pby\\ &=p(cx+by)\tag{5} \end{align} $$ Equation $(5)$ says that $p\mid b$.

Thus, assuming that $p$ is irreducible and $p\mid ab$, we have shown that if $p\nmid a$, then $p\mid b$.

QED