Require Import Classical.

Lemma LEM: forall p, p \/ ~p.
Proof.

(* Proof 1
intro. classical_left. apply NNPP. assumption. *)

(* Proof 2
intro. classical_right. assumption. *)

(* Proof 3 *)
intro. tauto.
Qed.

(* NNPP used in Proof 1 above is essentially the
double-negation elimination rule of Natural Deduction for
Classical Logic.

In the following, prove that using LEM *)
Lemma nnpp : forall p, ~~p -> p.
Admitted.