Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Leonardo de Moura, Jeremy Avigad, Mario Carneiro
-/
import Std.Classes.Dvd

namespace Nat

/--
Divisibility of natural numbers. `a ∣ b` (typed as `\|`) says that
there is some `c` such that `b = a * c`.
-/
instance: Dvd Natinstance : Dvd: Type ?u.2 → Type ?u.2Dvd Nat: TypeNat := ⟨fun a: ?m.10a b: ?m.13b => ∃ c: ?m.18c, b: ?m.13b = a: ?m.10a * c: ?m.18c⟩

/-- Sum of a list of natural numbers. -/
protected def sum: List Nat → Natsum (l: List Natl : List: Type ?u.92 → Type ?u.92List Nat: TypeNat) : Nat: TypeNat := l: List Natl.foldr: {α : Type ?u.98} → {β : Type ?u.97} → (α → β → β) → β → List α → βfoldr (·+·): Nat → Nat → Nat(·+·) 0: ?m.1510

/--
Integer square root function. Implemented via Newton's method.
-/
def sqrt: Nat → Natsqrt (n: Natn : Nat: TypeNat) : Nat: TypeNat :=
if n: Natn ≤ 1: ?m.3901 then n: Natn else
iter: Nat → Nat → Natiter n: Natn (n: Natn / 2: ?m.4272)
where
/-- Auxiliary for `sqrt`. If `guess` is greater than the integer square root of `n`,
returns the integer square root of `n`. -/
iter: Nat → Nat → Natiter (n: Natn guess: Natguess : Nat: TypeNat) : Nat: TypeNat :=
let next: ?m.253next := (guess: Natguess + n: Natn / guess: Natguess) / 2: ?m.2642
if _h: ?m.381_h : next: ?m.253next < guess: Natguess then
iter: Nat → Nat → Natiter n: Natn next: ?m.253next
else
guess: Natguess
termination_by iter guess => guess: ?αguess
```