Yes, I realize this arguments cuts both ways. One way is that you can write all these theorems in constructive logic, so there is no need for classical axioms. And the other way, is that users should freely use classical axioms because they can be mechanically removed.
Myself, I've never seen an automated theorem prover that will perform this sort of translation automatically. I have, on rare occasion, gone through by hand to remove uses of classical axioms in Coq proofs of theorems than ought not to be using them. Usually the uses are pretty superficial.
How difficult would it be to write a Coq plugin to perform these translations?
The thing I like about Coq is that it appears to have better tooling than the other theorem provers (coqtop, proof-general for emacs), and you can extract code for other programming languages. I haven't looked in great detail at the alternatives though.
Myself, I've never seen an automated theorem prover that will perform this sort of translation automatically. I have, on rare occasion, gone through by hand to remove uses of classical axioms in Coq proofs of theorems than ought not to be using them. Usually the uses are pretty superficial.