Is this proof fundamentally impossible in Coq? (without resorting to Sigma types)

puzzle.v

Require Import Coq.Lists.List.
Require Import Coq.micromega.Lia.
Import ListNotations.
Arguments In {_}.

Lemma problem N (P : nat -> Prop) (Q : nat -> nat -> Prop) :
  (forall n : nat, P n -> n <= N) ->
  (forall n : nat, n <= N -> exists x, Q n x) ->
  exists l : list nat, forall n, P n -> exists x, In x l /\ Q n x.
Proof.
intros H1 H2; induction N.
- assert(H0: 0 <= 0). lia. apply H2 in H0 as [x Px].
  exists [x]. intros n Hn. apply H1 in Hn. exists x. split. simpl. now left.
  now replace n with 0 by lia.
- (* STUCK *)
Admitted.