The proof (at least the proof I know) that a principal ideal domain is a unique factorization domain uses the axiom of choice in multiple ways, and the usual way to show that a Euclidean domain is a UFD is to show that it's a PID (which is easy and constructive).
Is there a direct proof, not using the axiom of choice, that a Euclidean domain is a UFD?