Using the law of the excluded middle is definitely a shortcut in such proofs, but there is no proof I'm aware of that shows no comparable constructive proof is

Using the law of the excluded middle is definitely a shortcut in such proofs, but there is no proof I'm aware of that shows no comparable constructive proof is possible. We reason with non-computable objects all of the time, such constructions are simply never fully materialized, and the need to materialize them are typically eliminated in later stages to prove concrete results. It's a good example but I don't think it's sufficient to exclude math from computer science.