sqrt

See [Wikipedia, Methods of computing square roots] (https://en.wikipedia.org/wiki/Methods_of_computing_square_roots#Binary_numeral_system_(base_2)).

theorem Nat.sqrt_le (n : Nat) : n.sqrt * n.sqrt ≤ n

theorem Nat.lt_succ_sqrt (n : Nat) : n < n.sqrt.succ * n.sqrt.succ