'How to prove in Coq ~~(P \/ ~P)

I want to prove ~~(P \/ ~P) in Coq, which sounds somehow trivial... However I do not know where to go since there is not any single hypothesis. I have written the following code which is not working, since it is giving the following exception [ltac_use_default] expected after [tactic] (in [tactic_command]).

Parameter P: Prop.

Section r20.
Lemma regra1: ~~(P \/ ~P).
Proof.
  intro.
   - cut P.
   - cut ~P
Qed.
End r20.
logiccoq


Sources

This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.

Source: Stack Overflow

Solution Source

Related Questions