I'm currently showing a few things about $\mathbb{N}$ in the proof assistant Coq, with the goal to take these proofs and turn them into deductions in the first-order theory of PA.
One of the open goals right now is the implication "irreducible $\Rightarrow$ prime". Looking for proofs on this site and elsewhere on the web, I have so far only found proofs using the $\operatorname{gcd}$ plus Bézout's Lemma or ideals, everything taking place in $\mathbb{Z}$. The fact that they are shown for $\mathbb{Z}$ is not per se a problem, since it should be possible to show something like this: $$ PA \vdash \forall x y ~ \exists ab ~~a x = by \, + \, \operatorname{gcd}(x,y) ~\lor ~ ay = bx \, + \, \operatorname{gcd}(x,y) $$ which would be a translation of Bézout into PA. One could then continue from there.
However I feel that PA should be strong enough to circumvent the necessity to define and develop results about the $\operatorname{gcd}$ just to prove this implication. Since my attempts so far have not been fruitful, any hint for a different approach would be very welcome.
Bonus points if the proof is in Heyting Artihmetic instead of PA.
I now found a proof in this document (Proposition $1.4$) which uses strong induction. The statement on which the induction is used can be simplified slightly, which I will present here for completeness. The proof also needs Euclid's lemma and the following fact about divisibility which can be shown by induction on $a$:
Proof: Assume that $x$ is irreducible and try to show $x \vert a b ~\Rightarrow~ x \vert a ~\lor ~ x \vert b~$ by strong induction on $a$. We distinguish two cases:
($x \leq a$) By Euclid we have $a = d x +r$, with $r < x$ implying $r < a$. Since we have $$ x \vert ab ~\Longrightarrow~ x \vert (dxb + r b) ~\stackrel{\text{Lemma}}{\Longrightarrow}~ x \vert rb $$ the induction hypothesis can be applied on $r$ giving us $~x \vert r ~\lor~ x \vert b~$, which shows $~x \vert a ~\lor~ x \vert b$.
($x > a$) It is trivial for $a = 0$, so assume $a > 0$. In this case Euclid gives us $x = da +r$ with $r<a$. Since $~x \vert ab~$ there is a $k$ with $kx = ab$. So we have $$ x \vert xb ~\Longrightarrow ~ x \vert (dab + rb) ~\Longrightarrow~ x \vert (dkx + rb) ~\stackrel{\text{Lemma}}{\Longrightarrow}~ x \vert rb $$ again making it possible to apply the induction hypothesis on $r$ to get $~x \vert r ~\lor~ x \vert b~$. If $~x\vert b~$ we are done. If $~x \vert r~$ we must actually have $r = 0$ since $r < a < x$. Thus $x = da$ and by the irreducibility of $x$ we get $a = x ~\lor~ a = 1$ showing $~ x \vert a ~\lor~ x \vert b$ respectively.
tl;dr of the proof: Depending on whether $x \leq a$ or $x > a$ we do the divisions $a / x$ or $x / a$ with remainder and use strong induction on the remainder.