P /\ Q <-> ~(P -> ~Q)

Connectives.v

Require Import Coq.Logic.Classical.

Theorem conj_iff :
  forall P Q, P /\ Q <-> ~(P -> ~Q).
Proof.
  split.
  unfold not.
  intros (HP,HQ) H.
  apply H.
  apply HP.
  apply HQ.

  intros H.
  assert (P \/ ~P) as HP by apply classic.
  destruct HP as [HP|HNP].

  split.
  assumption.
  assert (Q \/ ~Q) as HQ by apply classic.
  destruct HQ as [HQ|HNQ].
  assumption.
  exfalso.
  apply H.
  intros.
  assumption.

  exfalso.
  apply H.
  intros.
  contradiction.
Qed.