Erdős Problem 779

Reference: erdosproblems.com/779

theorem erdos_779 (n : ℕ) (hn : n ≥ 1) : let P := ∏ i ∈ Finset.range (n + 1), Nat.nth Nat.Prime i; ∃ (p : ℕ), Nat.Prime p ∧ Nat.Prime (P + p) ∧ Nat.nth Nat.Prime n < p ∧ p < P

A Conjecture of Marian Deaconescu, see p.120 in https://doi.org/10.2307/2975810

[Needed to index shift in order to avoid trivial case $n = 0$, where the conjecture is trivially false.]