open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product
open import Data.Bool hiding (_<_; _≤_)

infix 4 _sqrtof_
_sqrtof_ : ℕ → ℕ → Set _
_sqrtof_ x y = (x * x ≤ y) × (y < suc x * suc x)

⌊√_⌋ : ℕ → ℕ
⌊√ x ⌋ = f x x
  where
  f : ℕ → ℕ → ℕ
  f 0 _ = 0
  f (suc r) n with (r * r) <ᵇ suc n 
  ...      | true = r
  ...      | false = f r n

thm : ∀ x → ⌊√ x ⌋ sqrtof x
thm = ?