feat(data/int/basic): sign raised to an odd power (#7559)

Since sign is either -1, 0, or 1, it is unchanged when raised to an odd power.



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

Author: tb65536

src/data/int/basic.lean

@@ -818,6 +818,12 @@ theorem mul_sign : ∀ (i : ℤ), i * sign i = nat_abs i
 | 0       := mul_zero _
 | -[1+ n] := mul_neg_one _
 
+@[simp]
+theorem sign_pow_bit1 (k : ℕ) : ∀ n : ℤ, n.sign ^ (bit1 k) = n.sign
+| (n+1:ℕ) := one_pow (bit1 k)
+| 0       := zero_pow (nat.zero_lt_bit1 k)
+| -[1+ n] := (neg_pow_bit1 1 k).trans (congr_arg (λ x, -x) (one_pow (bit1 k)))
+
 theorem le_of_dvd {a b : ℤ} (bpos : 0 < b) (H : a ∣ b) : a ≤ b :=
 match a, b, eq_succ_of_zero_lt bpos, H with
 | (m : ℕ), ._, ⟨n, rfl⟩, H := coe_nat_le_coe_nat_of_le $