Proof in coq - Predicate logic

Question

Trying to prove the following in coq: Prove that the universal quantifier distributes over conjunction ∀x ∈ A, P x ∧ Qx ⇐⇒ (∀x ∈ A, P x) ∧ (∀x ∈ A, Qx)

My Proof so far-

Parameter (A : Type).
Parameter (P Q : A -> Prop).

Lemma II3: (forall x : A, P x /\ Q x) <->
           (forall x : A, P x) /\ (forall x : A, Q x).
split.
intro H.
split.
apply H.
intros H1.
Proof.

I have tried to split, destruct, and introduce a new hypothesis, but I just can't seem to make it past this point. Any advice would be greatly appreciated.

Answer 1

this is a pretty easy proof, for example now intuition; apply H will solve your goal.

In your case, you should first figure out how the proof works using pen and paper, and once you've done that, the proof in Coq will be trivial.