Further lemmas about the integers

The distinction between this file and Mathlib/Data/Int/Order/Basic.lean is not particularly clear. They are separated by now to minimize the porting requirements for tactics during the transition to mathlib4. Please feel free to reorganize these two files.

nat abs

theorem Int.natAbs_eq_iff_mul_self_eq {a b : ℤ} : a.natAbs = b.natAbs ↔ a * a = b * b

theorem Int.natAbs_lt_iff_mul_self_lt {a b : ℤ} : a.natAbs < b.natAbs ↔ a * a < b * b

theorem Int.natAbs_le_iff_mul_self_le {a b : ℤ} : a.natAbs ≤ b.natAbs ↔ a * a ≤ b * b

Integer sqrt

theorem Int.abs_le_sqrt {a b : ℤ} (hn : 0 ≤ b) : |a| ≤ sqrt b ↔ a * a ≤ b

theorem Int.abs_le_sqrt_iff_sq_le {a b : ℤ} (hn : 0 ≤ b) : |a| ≤ sqrt b ↔ a ^ 2 ≤ b