Theorem: pn_pn_plus_one (PrimeNumberTheoremAnd/Consequences.lean)

State before:
⊢ ∃ c, (c =o[atTop] fun x => 1) ∧ ∀ (n : ℕ), ↑(nth Nat.Prime (n + 1)) - ↑(nth Nat.Prime n) = c n * ↑(nth Nat.Prime n)
Tactic:
sorry
State after:
no goals