-- There is always a prime between n² and (n+1)² for every positive n. theorem legendre (n : ℕ) (hn : 0 < n) : ∃ p : ℕ, n^2 < p ∧ p < (n + 1)^2 ∧ Nat.Prime p :=