How to use Coq to prove a logical equivalence?

142 Views Asked by At

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].