Properties of the natural number square root function.

sqrt

See [Wikipedia, Methods of computing square roots] (https://en.wikipedia.org/wiki/Methods_of_computing_square_roots#Binary_numeral_system_(base_2)).

@[irreducible]

theorem Nat.sqrt.iter_sq_le (n guess : ℕ) : iter n guess * iter n guess ≤ n

@[irreducible]

theorem Nat.sqrt.lt_iter_succ_sq (n guess : ℕ) (hn : n < (guess + 1) * (guess + 1)) : n < (iter n guess + 1) * (iter n guess + 1)

theorem Nat.sqrt_le (n : ℕ) : n.sqrt * n.sqrt ≤ n

theorem Nat.sqrt_le' (n : ℕ) : n.sqrt ^ 2 ≤ n

theorem Nat.lt_succ_sqrt (n : ℕ) : n < n.sqrt.succ * n.sqrt.succ

theorem Nat.lt_succ_sqrt' (n : ℕ) : n < n.sqrt.succ ^ 2

theorem Nat.sqrt_le_add (n : ℕ) : n ≤ n.sqrt * n.sqrt + n.sqrt + n.sqrt

theorem Nat.le_sqrt {m n : ℕ} : m ≤ n.sqrt ↔ m * m ≤ n

theorem Nat.le_sqrt' {m n : ℕ} : m ≤ n.sqrt ↔ m ^ 2 ≤ n

theorem Nat.sqrt_lt {m n : ℕ} : m.sqrt < n ↔ m < n * n

theorem Nat.sqrt_lt' {m n : ℕ} : m.sqrt < n ↔ m < n ^ 2

theorem Nat.sqrt_le_self (n : ℕ) : n.sqrt ≤ n

theorem Nat.sqrt_le_sqrt {m n : ℕ} (h : m ≤ n) : m.sqrt ≤ n.sqrt

@[simp]

theorem Nat.sqrt_zero : sqrt 0 = 0

@[simp]

theorem Nat.sqrt_one : sqrt 1 = 1

theorem Nat.sqrt_eq_zero {n : ℕ} : n.sqrt = 0 ↔ n = 0

theorem Nat.eq_sqrt {n a : ℕ} : a = n.sqrt ↔ a * a ≤ n ∧ n < (a + 1) * (a + 1)

theorem Nat.eq_sqrt' {n a : ℕ} : a = n.sqrt ↔ a ^ 2 ≤ n ∧ n < (a + 1) ^ 2

theorem Nat.le_three_of_sqrt_eq_one {n : ℕ} (h : n.sqrt = 1) : n ≤ 3

theorem Nat.sqrt_lt_self {n : ℕ} (h : 1 < n) : n.sqrt < n

theorem Nat.sqrt_pos {n : ℕ} : 0 < n.sqrt ↔ 0 < n

theorem Nat.sqrt_add_eq {a : ℕ} (n : ℕ) (h : a ≤ n + n) : (n * n + a).sqrt = n

theorem Nat.sqrt_add_eq' {a : ℕ} (n : ℕ) (h : a ≤ n + n) : (n ^ 2 + a).sqrt = n

theorem Nat.sqrt_eq (n : ℕ) : (n * n).sqrt = n

theorem Nat.sqrt_eq' (n : ℕ) : (n ^ 2).sqrt = n

theorem Nat.sqrt_succ_le_succ_sqrt (n : ℕ) : n.succ.sqrt ≤ n.sqrt.succ

theorem Nat.exists_mul_self (x : ℕ) : (∃ (n : ℕ), n * n = x) ↔ x.sqrt * x.sqrt = x

theorem Nat.exists_mul_self' (x : ℕ) : (∃ (n : ℕ), n ^ 2 = x) ↔ x.sqrt ^ 2 = x

theorem Nat.sqrt_mul_sqrt_lt_succ (n : ℕ) : n.sqrt * n.sqrt < n + 1

theorem Nat.sqrt_mul_sqrt_lt_succ' (n : ℕ) : n.sqrt ^ 2 < n + 1

theorem Nat.succ_le_succ_sqrt (n : ℕ) : n + 1 ≤ (n.sqrt + 1) * (n.sqrt + 1)

theorem Nat.succ_le_succ_sqrt' (n : ℕ) : n + 1 ≤ (n.sqrt + 1) ^ 2

theorem Nat.not_exists_sq {m n : ℕ} (hl : m * m < n) (hr : n < (m + 1) * (m + 1)) : ¬∃ (t : ℕ), t * t = n

There are no perfect squares strictly between m² and (m+1)²

theorem Nat.not_exists_sq' {m n : ℕ} : m ^ 2 < n → n < (m + 1) ^ 2 → ¬∃ (t : ℕ), t ^ 2 = n