have hn : a < (a + 1) * (a + 1) := calc
  a ≤ a * a             := le_mul_self a
  _ < a * a + 1         := lt_add_one (a * a)
  _ ≤ (a + 1) * (a + 1) := by simp [add_mul_self_eq]
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a : M
this : a < (a + 1) * (a + 1) → ∃ x, x * x ≤ a ∧ a < (x + 1) * (x + 1)
⊢ ∃ x, x * x ≤ a ∧ a < (x + 1) * (x + 1)
M : Type u_1
inst✝⁶ : Zero M
inst✝⁵ : One M
inst✝⁴ : Add M
inst✝³ : Mul M
inst✝² : LT M
inst✝¹ : M ⊧ₘ* 𝐏𝐀⁻
inst✝ : M ⊧ₘ* 𝐈open
a : M
this : a < (a + 1) * (a + 1) → ∃ x, x * x ≤ a ∧ a < (x + 1) * (x + 1)
hn : a < (a + 1) * (a + 1)
⊢ ∃ x, x * x ≤ a ∧ a < (x + 1) * (x + 1)