These are lemmas that were proved in the process of porting Data.Nat.Sqrt.

theorem Nat.mul_le_of_le_div (k : ℕ) (x : ℕ) (y : ℕ) (h : x ≤ y / k) : x * k ≤ y

theorem Nat.div_mul_div_le (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) : a / b * (c / d) ≤ a * c / (b * d)

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

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