Coq - Universal quantifiers in hypoteses

Question

I would like to prove the following theorem

Goal (forall x, P x \/ Q x) -> (forall x, P x) \/ (forall x, Q x).

with context

1 subgoal
P : nat -> Prop
Q : nat -> Prop
R : nat -> nat -> Prop
H : forall x : nat, P x \/ Q x
______________________________________(1/1)
(forall x : nat, P x) \/ (forall x : nat, Q x)

The statement seems to be correct in predicate logic, but I have no idea of how to prove it. The problem is essentially that I cannot eliminate all the forall at once, but I cannot neither apply left or right before destructing the hypotesis H.

Is there a straightforward way for doing that?

Answer 1

Take P to be evenness, Q to be oddity, and you should see that your theorem is flawed.