Proving tautology with coq

Question

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.