Learning coq, not sure what the error means NNPP

Question

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?

Answer 1

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.