feat(data/int/basic): Units are either equal or negatives of each other (#14517)

This PR adds a lemma stating that units in the integers are either equal or negatives of each other. I have found this lemma to be useful for casework.

Author: tb65536

src/data/int/basic.lean

@@ -1315,6 +1315,13 @@ begin
   { exact is_unit_one.neg }
 end
 
+lemma is_unit_eq_or_eq_neg {a b : ℤ} (ha : is_unit a) (hb : is_unit b) : a = b ∨ a = -b :=
+begin
+  rcases is_unit_eq_one_or hb with rfl | rfl,
+  { exact is_unit_eq_one_or ha },
+  { rwa [or_comm, neg_neg, ←is_unit_iff] },
+end
+
 lemma eq_one_or_neg_one_of_mul_eq_one {z w : ℤ} (h : z * w = 1) : z = 1 ∨ z = -1 :=
 is_unit_iff.mp (is_unit_of_mul_eq_one z w h)