sqrt n is the square root of a natural number n. If n is not a perfect square, it returns the largest k:ℕ such that k*k ≤ n.