证明素数存在无穷多个的Lean-Lang表示

import Mathlib

-- 试证明素数有无穷多个
theorem infinite_prime_official_version : ∀ N : Nat , ∃ p,  p ≥ N ∧  Nat.Prime p := by
 exact Nat.exists_infinite_primes