Lemmas about divisibility of powers

theorem Int.dvd_pow {a b : Int} {n : Nat} (hab : b ∣ a) : b ^ n ∣ a ^ n

theorem Int.ediv_pow {a b : Int} {n : Nat} (hab : b ∣ a) : (a / b) ^ n = a ^ n / b ^ n

theorem Int.tdiv_pow {a b : Int} {n : Nat} (hab : b ∣ a) : a.tdiv b ^ n = (a ^ n).tdiv (b ^ n)

theorem Int.fdiv_pow {a b : Int} {n : Nat} (hab : b ∣ a) : a.fdiv b ^ n = (a ^ n).fdiv (b ^ n)