Answer to auggierose's comment above: Yes you can prove that sqrt(2) is irrational.
This is actually a great example, because it doesn't need excluded middle. Equality of rational numbers is decidable, which means that classical reasoning is provable. And yes, even if it wasn't, it would still work.
Edit: Ok, this was apparently confusing, so let me repeat it here. Yes, the same proof works. This form of excluded middle is entirely unproblematic.
There might be some confusion. The typical proof of the irrationality of root 2 is phrased as a proof-by-contradiction, and I've come across folk who mistakenly think that this technique is exclusive to classical mathematics.
In fact, the standard proof-by-contradiction that sqrt(2) is irrational is also intuitionistically valid. The important point for this case is that we're proving a negative property (irrationality), so this sort of proof by contradiction is fine.
The standard example of a classical proof I use is the one showing that there exist irrationals x and y such that x^y is rational. The dead easy proof asks whether x^y is rational for x=y=sqrt(2). If it is, we're done. Otherwise, we just take x=sqrt(2)^sqrt(2) and y=sqrt(2).
But note that we don't actually know for sure which x and y work, so this is definitely classical. An intuitionistic proof here would have to tell us directly what x and what y work.
This is actually a great example, because it doesn't need excluded middle. Equality of rational numbers is decidable, which means that classical reasoning is provable. And yes, even if it wasn't, it would still work.
Edit: Ok, this was apparently confusing, so let me repeat it here. Yes, the same proof works. This form of excluded middle is entirely unproblematic.