Proving tautology with coq
You cannot prove it in "vanilla" Coq, because it is based on intuitionistic logic:


  From a proof-theoretic perspective, intuitionistic logic is a restriction of classical logic in which the law of excluded middle and double negation elimination are not valid logical rules.


There are several ways you can deal with a situation like this.


Introduce the law of excluded middle as an axiom:

Axiom excluded_middle : forall P:Prop, P \/ ~ P.


There is no more need to prove anything after this point.
Introduce some axiom equivalent to the law of excluded middle and prove their equivalence. Here is just a few examples.


Double negation elimination is one such axiom: 

Axiom dne : forall P:Prop, ~~P -&gt; P.

Peirce's law is another example:

Axiom peirce : forall P Q:Prop, ((P -&gt; Q) -&gt; P) -&gt; P.

Or use one of the De Morgan's laws:

Axiom de_morgan_and : forall P Q:Prop, ~(~P /\ ~Q) -&gt; P \/ Q.