feat(data/int/basic): add lemmas for w*z = -1 (#17478)
This small PR adds two lemmas:
```lean
lemma eq_one_or_neg_one_of_mul_eq_neg_one {z w : ℤ} (h : z * w = -1) : z = 1 ∨ z = -1
lemma eq_one_or_neg_one_of_mul_eq_neg_one' {z w : ℤ} (h : z * w = -1) : z = 1 ∧ w = -1 ∨ z = -1 ∧ w = 1
```
that are analogous to the existing `eq_one_or_neg_one_of_mul_eq_one` and `eq_one_or_neg_one_of_mul_eq_one'`.
On request by Eric Wieser, this also adds
```lean
lemma mul_eq_neg_one_iff_eq_one_or_neg_one {z w : ℤ} : z * w = -1 ↔ z = 1 ∧ w = -1 ∨ z = -1 ∧ w = 1
```
and its analogue
```lean
lemma mul_eq_one_iff_eq_one_or_neg_one {z w : ℤ} : z * w = 1 ↔ z = 1 ∧ w = 1 ∨ z = -1 ∧ w = -1
```
