English
If n < (guess + 1)^2, then n < (sqrt.iter(n, guess) + 1)^2.
Русский
Если n < (guess + 1)^2, то n < (sqrt.iter(n, guess) + 1)^2.
LaTeX
$$$n < (\text{guess} + 1)^2 \Rightarrow n < (\mathrm{sqrt.iter}(n, \text{guess}) + 1)^2$$$
Lean4
theorem lt_iter_succ_sq (n guess : ℕ) (hn : n < (guess + 1) * (guess + 1)) :
n < (sqrt.iter n guess + 1) * (sqrt.iter n guess + 1) :=
by
unfold sqrt.iter
let m := (guess + n / guess) / 2
dsimp
split_ifs with h
· suffices n < (m + 1) * (m + 1) by simpa only [dif_pos h] using sqrt.lt_iter_succ_sq n m this
refine Nat.lt_of_mul_lt_mul_left ?_ (a := 4 * (guess * guess))
apply Nat.lt_of_le_of_lt AM_GM
rw [show (4 : ℕ) = 2 * 2 from rfl]
rw [Nat.mul_mul_mul_comm 2, Nat.mul_mul_mul_comm (2 * guess)]
refine Nat.mul_self_lt_mul_self (?_ : _ < _ * ((_ / 2) + 1))
rw [← add_div_right _ (by decide), Nat.mul_comm 2, Nat.mul_assoc,
show guess + n / guess + 2 = (guess + n / guess + 1) + 1 from rfl]
have aux_lemma {a : ℕ} : a ≤ 2 * ((a + 1) / 2) := by omega
refine lt_of_lt_of_le ?_ (Nat.mul_le_mul_left _ aux_lemma)
rw [Nat.add_assoc, Nat.mul_add]
exact Nat.add_lt_add_left (lt_mul_div_succ _ (lt_of_le_of_lt (Nat.zero_le m) h)) _
· exact hn
