no goals
n m : ℕ
hl : m ^ 2 < n
hr : n < (m + 1) ^ 2
⊢ ¬∃ t, t ^ 2 = n
simpa only [pow_two] using
  not_exists_sq (by simpa only [pow_two] using hl) (by simpa only [pow_two] using hr)
no goals
n m : ℕ
hl : m ^ 2 < n
hr : n < (m + 1) ^ 2
⊢ ?m.11299 * ?m.11299 < n
simpa only [pow_two] using hl
no goals
n m : ℕ
hl : m ^ 2 < n
hr : n < (m + 1) ^ 2
⊢ n < (m + 1) * (m + 1)
simpa only [pow_two] using hr