title: How to prove (forall x, P x /\ Q x) -> (forall x, P x)
body: <p>How does one prove (forall x, P x /\ Q x) -> (forall x, P x) in Coq? Been trying for hours and can't figure out how to break down the antecedent to something that Coq can digest. (I'm a newb, obviously :)</p>