Как доказать следующее в Coq?

Question

Как доказать следующее в Coq?

(p-> q) -> (~ q-> ~ p)

Вот с чего я начал:

Lemma work : (forall p q : Prop, (p->q)->(~q->~p)).
Proof.
  intros p q.
  intros p_implies_q not_q.
  intros p_true.