proposition: Lemma not_and_eq : forall P Q : Prop, ~(P /\ Q) <-> ~P \/ ~Q.
proof: Proof. split; intro. destruct (classic P). right. intro. absurd (P/\Q). hyp. auto. left. auto. intros [h1 h2]. destruct H. absurd P; hyp. absurd Q; hyp. Qed.
imports: CoLoR(LogicUtil)