Hope that helps This is an example that the quality of an SO question is many times determined by an answer, not the question. I kind of give this answer to thank M.Eberl for another useful answer, since I can't make comments.

As to a comment above, that you may be asking a homework question, the comment is valid, but if you're confused by negation, then you're mostly doomed anyway, until you make progress, so even one complete answer wouldn't help you, and here, there's no right answer.

code :

```
lemma "~(P ∧ Q) ==> Q --> ~P"
by auto
```

```
lemma disj_not2: "(P | ~Q) = (Q --> P)"
```

```
lemma "~(P ∧ Q) ==> Q --> ~P"
proof-
fix P Q :: bool
assume "~(P ∧ Q)"
hence "~P ∨ ~Q" by simp
hence "~Q ∨ ~P" by metis
thus "Q --> ~P" by metis
qed
```