Is possible to prove undecidability of the halting problem in Coq?

Question

I was watching the "Five Stages of Accepting Constructive Mathematics" by Andrej Bauer and he says that there is two kinds of proof by contradiction (or two things that mathematicians call proof by contradiction):

1. Assume $P$ is false... blah blah blah, contradiction. Therefore $P$ is true.
2. Assume $P$ is true... blah blah blah, contradiction. Therefore $P$ is false.

The first one is equivalent to the Law of Excluded Middle (LEM) and the second one is to how prove negation.

The proof of the undecidability of the Halting Problem (HP) is a proof by contradiction: assume there is a machine $D$ that can decide the HP... blah blah blah, contradiction. Therefore $D$ does not exist.

So, let $P$ be "$D$ exists and can decide the HP". Assume $P$ is true... blah blah blah, contradiction. Therefore $P$ is false.

This looks like the second kind of proof by contradiction, so is possible to prove the undecidability of the halting-problem in Coq (without assuming LEM)?

EDIT: I would to see some points about proving this using contradiction. I know that this can also be proved using diagonalization.