Can anyone break down the following and show how to prove the following in Coq?
(q V p) ∧ (¬p -> q) <-> (p V q).
Here is what I started with in Coq:
Lemma work: (forall p q: Prop, (q \/ p)/\(~p -> q) <-> (p \/ q)).
Proof.
split.
intros H.
destruct H as [H1 H2].