Comparisons between rational approximations to the square root of a natural number and the real square root.

theorem Nat.ratSqrt_le_realSqrt (x : ℕ) {prec : ℕ} (h : 0 < prec) : ↑(x.ratSqrt prec) ≤ √↑x

theorem Nat.realSqrt_lt_ratSqrt_add_inv_prec (x : ℕ) {prec : ℕ} (h : 0 < prec) : √↑x < ↑(x.ratSqrt prec) + 1 / ↑prec

theorem Nat.realSqrt_mem_Ico (x : ℕ) {prec : ℕ} (h : 0 < prec) : √↑x ∈ Set.Ico (↑(x.ratSqrt prec)) (↑(x.ratSqrt prec) + 1 / ↑prec)

theorem Nat.ratSqrt_mem_Ioc (x : ℕ) {prec : ℕ} (h : 0 < prec) : ↑(x.ratSqrt prec) ∈ Set.Ioc (√↑x - 1 / ↑prec) √↑x