feat(data/int/basic): Lemmas for when a square equals 1 (#14501)

This PR adds two lemmas for when a square equals one. The `lt` lemma will be useful for irreducibility of x^n-x-1.



Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

src/data/int/basic.lean

@@ -1604,6 +1604,13 @@ begin
   exact lt_of_lt_of_le h2 (le_abs_self m),
 end
 
+lemma sq_eq_one_of_sq_lt_four {x : ℤ} (h1 : x ^ 2 < 4) (h2 : x ≠ 0) : x ^ 2 = 1 :=
+sq_eq_one_iff.mpr ((abs_eq (@zero_le_one ℤ _)).mp (le_antisymm (lt_add_one_iff.mp
+  (abs_lt_of_sq_lt_sq h1 zero_le_two)) (sub_one_lt_iff.mp (abs_pos.mpr h2))))
+
+lemma sq_eq_one_of_sq_le_three {x : ℤ} (h1 : x ^ 2 ≤ 3) (h2 : x ≠ 0) : x ^ 2 = 1 :=
+sq_eq_one_of_sq_lt_four (lt_of_le_of_lt h1 (lt_add_one 3)) h2
+
 end int
 
 attribute [irreducible] int.nonneg