I don't have time at the moment to give a proof in Coq or another constructive proof assistant, but it boils down to the fact that "n is even and n is odd impli

I don't have time at the moment to give a proof in Coq or another constructive proof assistant, but it boils down to the fact that "n is even and n is odd implies n = 17" is a function that can never be executed.