thm : ∀ x → ⌊√ x ⌋ sqrtof x
thm 0 = z≤n , s≤s (z≤n)
thm (suc n) = thmˡ , thmʳ
  where
  x : ℕ
  x = ⌊√ suc n ⌋
  y : ℕ
  y = suc n

  ihˡ : ⌊√ n ⌋ * ⌊√ n ⌋ ≤ n
  ihˡ = proj₁ (thm n)

  thmˡ : x * x ≤ y
  thmˡ = ?


  thmʳ : y < suc x * suc x
  thmʳ = ?