Q:

Learning coq, not sure what the error means NNPP

So i've just started to learn coq (and it is way over my head so far) and I'm trying to do a basic proof and I'm pretty lost, found some help so far but what I think I'm supposed to do coq throws an error. So in my editor part I have:
Section wut.
Variables p q: Prop.
Theorem T1 : (~q->~p)->(p->q).
Proof.
intros.
apply NNPP.
intro.
apply H in H1.
contradiction.
Qed.

and in the Proofing box i have :
1 subgoal
p, q : Prop
H : ~ q -> ~ p
H0 : p
______________________________________(1/1)
q

and in the error box I have:
The reference NNPP was not found in the current environment.

what does it mean it can't be found in the current environment?

A:

The NNPP lemma is the principle of double-negation elimination: it says that ~ ~ P implies P.  To fix the error message, you must import the Coq library where NNPP is defined:
Require Import Coq.Logic.Classical.

Section wut.
Variables p q: Prop.
Theorem T1 : (~q->~p)->(p->q).
Proof.
intros.
apply NNPP.
intro.
apply H in H1.
contradiction.
Qed.

