The thing here is that this uses the law of the excluded middle: a proposition is either true or false, there is no other possibility. That's the basis of a proof using reduction ad absurdum. But that's not part of Coq (or any P.A. based on constructive logic) by default. If one is not aware of this indeed doing this proof will be impossible in Coq. This said Coq can work with the law of excluded middle (so support classical logic), but you have to explicitly assert it and use it.
This being said, I haven't tried this proof in Coq ;) Just seeing this point as something to take into account, and that may be a problem for some people new to Coq and not aware of it.
One explanation for why many people say that Euclid's proof is not a proof by contradiction is because you can actually get the second statement with only a little more care (i.e. n!+1 has a prime divisor, which is thus greater than n).
1) Proofs are well defined enough in the first place that you don't need great insight to understand them;
2) The time of some mathematicians is very invaluable;
3) Formalizing/verifying statements is sufficiently useful for mathematicians;
then they might be useful?
I would classify myself as a "proof programmer" who works with Metamath for much the same reasons as people use Coq (I just happen to prefer Metamath's set theory foundations to type theory). I find the article's claim "Set theory has sufficed as a foundation for more than a century, but it can’t readily be translated into a form that computers can use to check proofs" as outright false for this reason. Mizar is another set theory-based proof system.
If I wanted to prove x <= n -> x = 0 or x = 1 or ... or x = n, I would use http://us.metamath.org/mpegif/leloe.html to turn x <= n <-> x < n or x = n, and http://us.metamath.org/mpegif/zltlem1.html to prove x <= n-1 from x < n. Repeat until you get down to zero to get all n cases.
Think of all you need to prove that: the natural numbers, the definition of addition, subtraction, multiplication, division (and remainder), definition of cardinality/infinity (might not be necessary, if you just need proof that N doesn't divide any numbers between 2 and N-1) and a lot of formal logic
I remember seeing a presentation where someone challenged the viewer to write a simple proof of the infinitude of the primes. I recommend you try it. I studied math in college, have an interest in formal proofs, and have written Coq code, so surely I could bang out a simple proof like that. I think I got stuck when I wanted to claim, "Given a natural number n, x <= n implies x = 0 or x = 1 or ... or x = n". It's possible that I have more experience now and could complete that proof if I tried again, but this is really the kind of thing they teach on the first day of an introduction to proofs course. I can't see mathematicians using theorem provers until they're easier to work with.
So I sympathize with and am rooting for Voevodsky here: There's no reason why theorem provers have to be a pain to use - we just need better foundations, better tools, and more experience using them.