Formalize the Euclid–Fortunate prime coverage question (OEIS A067836)

### What is the conjecture

OEIS A067836 starts with $a(1)=2$. Before selecting the next term, multiply all terms already
produced. If that product is $P$, the next term is the gap between $P$ and the first prime strictly
greater than $P+1$.

The sequence begins

$$2,3,5,7,13,11,17,19,23,37,\ldots$$

For example, after the first two terms the product is $2\cdot3=6$; the first prime strictly greater
than $6+1$ is $11$, so the next gap is $11-6=5$.

OEIS asks the coverage question verbatim:

> Do all primes occur in the sequence?

Reference:

- [OEIS A067836](https://oeis.org/A067836)

This is different from the classical Fortunate-number conjecture: A067836 feeds every preceding
gap back into the next product instead of using successive primorials.

### Prerequisites needed

Mathlib's Bertrand theorem, finite intervals and filters, natural-number arithmetic, and primitive
recursion are sufficient. The local helper filters a finite Bertrand interval and takes its least
prime. No addition to `FormalConjecturesForMathlib` is needed.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-11

### Choose either option

- [x] I plan on adding this conjecture to the repository
- [ ] This issue is up for grabs: I would like to see this conjecture added by somebody else

Start by reading OEIS A067836 and the Mathlib Bertrand theorem, then inspect the repository's existing formal conjecture statements for patterns. Formalize the recursively defined sequence and its prime-coverage question using finite intervals, filters, least-prime selection, and primitive recursion; done means the conjecture statement compiles without adding to FormalConjecturesForMathlib.

Written by the indexing model from the issue text.