English
For x ∈ ℕ and prec > 0, x < (ratSqrt(x, prec) + 1/prec)^2.
Русский
Для натурального x и prec > 0 верно x < (ratSqrt(x, prec) + 1/prec)^2.
LaTeX
$$$ x < (\operatorname{ratSqrt}(x, \operatorname{prec}) + \frac{1}{\operatorname{prec}})^2, \quad (0 < \operatorname{prec}) $$$
Lean4
theorem lt_ratSqrt_add_inv_prec_sq (x : ℕ) {prec : ℕ} (h : 0 < prec) : x < (ratSqrt x prec + 1 / prec) ^ 2 :=
by
unfold ratSqrt
rw [← mul_lt_mul_iff_of_pos_right (a := (prec ^ 2 : ℚ)) (by positivity)]
rw [← mul_pow, add_mul]
rw [div_mul_cancel₀, div_mul_cancel₀]
· norm_cast
exact lt_succ_sqrt' (x * prec ^ 2)
all_goals norm_cast; positivity