Negation examples in Coq from Coq Art

ex5_3.v

(* exercise 5.3 from Coq Art *)

Lemma id_prop : forall P : Prop, P -> P.
Proof.
  intros P H; apply H.
Qed.

Theorem not_False : ~False.
Proof id_prop False.

Lemma P3Q :
  forall P Q : Prop, (((P -> Q) -> Q) -> Q) -> P -> Q.
Proof.
  intros P Q H H0.
  apply H; intros H1; apply H1; apply H0.
Qed.

Theorem triple_neg : forall P : Prop, ~ ~ ~ P -> ~ P.
Proof.
  intros P H; red.
  apply P3Q.
  apply H.
Qed.

Lemma imp_trans :
  forall P Q R : Prop, (P -> Q) -> (Q -> R) -> P -> R.
Proof.
  intros P Q R H H0 p.
  apply H0; apply H; apply p.
Qed.

Theorem contrap : forall P Q : Prop, (P -> Q) -> ~ Q -> ~ P.
Proof.
  unfold not.
  intros P Q.
  apply (imp_trans P Q False).
Qed.

Theorem imp_absurd :
  forall P Q R : Prop, (P -> Q) -> (P -> ~ Q) -> P -> R.
Proof.
  intros P Q R H Absurd p.
  elim (Absurd p).
  apply H; assumption.
Qed.

I used http://www.cse.chalmers.se/research/group/logic/TypesSS05/resources/coq/CoqArt/depprod/on_negation.html for help along with http://flint.cs.yale.edu/cs428/coq/doc/Reference-Manual012.html