Basic lemmas about the divisibility relation in ℤ involving powers.

@[simp]

theorem Int.sign_pow_bit1 (k : ℕ) (n : ℤ) : Int.sign n ^ bit1 k = Int.sign n

theorem Int.pow_dvd_of_le_of_pow_dvd {p : ℕ} {m : ℕ} {n : ℕ} {k : ℤ} (hmn : m ≤ n) (hdiv : ↑(p ^ n) ∣ k) : ↑(p ^ m) ∣ k

theorem Int.dvd_of_pow_dvd {p : ℕ} {k : ℕ} {m : ℤ} (hk : 1 ≤ k) (hpk : ↑(p ^ k) ∣ m) : ↑p ∣ m