iter_sq_le — Mathlib

English

For all n, guess ∈ ℕ, we have sqrt.iter n guess * sqrt.iter n guess ≤ n.

Русский

Для всех n, рекурсивная итерация корня sqrt.iter n guess не превосходит n по квадрату.

LaTeX

$$$\sqrt{\mathrm{iter}}(n,\text{guess}) \;\cdot\; \sqrt{\mathrm{iter}}(n,\text{guess}) \le n$$$

Lean4

theorem iter_sq_le (n guess : ℕ) : sqrt.iter n guess * sqrt.iter n guess ≤ n :=
  by
  unfold sqrt.iter
  let next := (guess + n / guess) / 2
  if h : next < guess then simpa only [next, dif_pos h] using sqrt.iter_sq_le n next
  else
    apply Nat.mul_le_of_le_div
    grind

Похожие утверждения