excluded middle law and Lemma

excluded_middle.v

Require Import Classical_Prop.
Require Import ClassicalFacts.

Definition NNPP' : forall P:Prop, 
   excluded_middle  -> (~ ~ P -> P)
:= 
  fun P em =>
  let e1 := em P in 
  match e1 with 
    | or_intror r => fun p  => False_ind P (p r)
    | or_introl l => fun _ => l 
  end
.

Definition Peirce' : 
  forall P:Prop, 
  excluded_middle -> ((P -> False) -> P) -> P
:= 
  fun P em H => 
    let e1 := em P in 
    match e1 with 
    | or_introl l => l 
    | or_intror r =>  H r 
    end 
  .