lean_workbook_plus_32733
ProvedProve that there is no perfect square between and .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_32733 (k : ℕ) : ¬ ∃ x : ℕ, k^2 < x^2 ∧ x^2 < (k + 1)^2 := by sorry
Source
Prove that there is no perfect square between and .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_32733 (k : ℕ) : ¬ ∃ x : ℕ, k^2 < x^2 ∧ x^2 < (k + 1)^2 := by sorry