Reto 4: Existen infinitos números primos
Demostrar que existen infinitos números primos.
Para ello, completar la siguiente teoría de Lean 4:
import Mathlib.Tactic import Mathlib.Data.Nat.Prime.Defs open Nat example (n : ℕ) : ∃ p, n ≤ p ∧ Nat.Prime p := by sorry