/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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 Nat
instance : 
Dvd: Type ?u.2 → Type ?u.2
Dvd 
Nat: Type
Nat := ⟨fun 
a: ?m.10
a 
b: ?m.13
b => ∃ 
c: ?m.18
c, 
b: ?m.13
b = 
a: ?m.10
a * 
c: ?m.18
c⟩

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

/--
Integer square root function. Implemented via Newton's method.
-/
def 
sqrt: Nat → Nat
sqrt (
n: Nat
n : 
Nat: Type
Nat) : 
Nat: Type
Nat :=
  if 
n: Nat
n ≤ 
1: ?m.390
1 then 
n: Nat
n else
  
iter: Nat → Nat → Nat
iter 
n: Nat
n (
n: Nat
n / 
2: ?m.427
2)
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 → Nat
iter (
n: Nat
n 
guess: Nat
guess : 
Nat: Type
Nat) : 
Nat: Type
Nat :=
    let 
next: ?m.253
next := (
guess: Nat
guess + 
n: Nat
n / 
guess: Nat
guess) / 
2: ?m.264
2
    if 
_h: ?m.381
_h : 
next: ?m.253
next < 
guess: Nat
guess then
      
iter: Nat → Nat → Nat
iter 
n: Nat
n 
next: ?m.253
next
    else
      
guess: Nat
guess
termination_by iter guess => 
guess: ?α
guess