It feels like the following Coq statement should be true constructively:
Require Import Decidable.
Lemma dec_search_nat_counterexample (P : nat -> Prop) (decH : forall i, decidable (P i))
: (~ (forall i, P i)) -> exists i, ~ P i.
If there were an upper bound, I'd expect to be able to show something of the form "suppose that not every i < N satisfies P i. Then there is an i < N where ~ P i". Indeed, you could actually write a function to find a minimal example by searching from zero.
Of course, there's not an upper bound for the original claim, but I feel like there should be an inductive argument to get there from the bounded version above. But I'm not clever enough to figure out how! Am I missing a clever trick? Or is there a fundamental reason that this cann't work, despite the well-orderedness of the natural numbers?
Reworked answer after Meven Lennon-Bertrand's comment
This statement is equivalent to Markov's principle with P and ~P exchanged. Since P is decidable we have P <-> (~ ~ P), so that one can do this replacement.
This paper (http://pauillac.inria.fr/~herbelin/articles/lics-Her10-markov.pdf) suggest that Markov's principle is not provable in Coq, since the author (one of the authors of Coq) suggests a new logic in this paper which allows to prove Markov's principle.
Old answer:
This is morally the "Limited Principle of Omniscience" - LPO (see https://en.wikipedia.org/wiki/Limited_principle_of_omniscience). It requires classical axioms to prove it in Coq - or you assert itself as an axiom.
See e.g.:
Require Import Coquelicot.Markov.
Check LPO.
Print Assumptions LPO.
Afair there is no standard library version of it.