Proving tautology with coq

Currently I have to learn Coq and don't know how to deal with an or :

As an example, as simple as it is, I don't see how to prove:

Theorem T0: x \/ ~x.

I would really appreciate it, if someone could help me.

For reference I use this cheat sheet.

Also an example of a proof I have in mind: Here for double negation:

Require Import Classical_Prop.

Parameters x: Prop.

Theorem T7: (~~x) -> x. 
intro H. 
apply NNPP. 
exact H. 
Qed.

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 -> P.

-
Peirce's law is another example:

Axiom peirce : forall P Q:Prop, ((P -> Q) -> P) -> P.

-
Or use one of the De Morgan's laws:

Axiom de_morgan_and : forall P Q:Prop, ~(~P /\ ~Q) -> P \/ Q.

StackExchange Computer Science Q#66508, answer score: 15