Emultiplicity four pow sub one

theorem emultiplicity_four_pow_sub_one (κ n : ℕ) :    emultiplicity 2 ((4 * 2 ^ κ + 1 : ℤ) ^ n - 1)      = (κ + 2 : ℕ) + emultiplicity 2 (n : ℤ) := by  have hodd : Odd (4 * 2 ^ κ + 1 : ℤ) := ⟨2 * 2 ^ κ, by ring⟩  have hx : ¬ (2 : ℤ) ∣ (4 * 2 ^ κ + 1) := by rcases hodd with ⟨m, hm⟩; omega  have hxy : (4 : ℤ) ∣ (4 * 2 ^ κ + 1) - 1 := ⟨2 ^ κ, by ring⟩  have hsub : (4 * 2 ^ κ + 1 : ℤ) - 1 = 2 ^ (κ + 2) := by rw [pow_add]; ring  have h := Int.two_pow_sub_pow' (x := 4 * 2 ^ κ + 1) (y := 1) n hxy hx  rw [one_pow, hsub, emultiplicity_pow_self_of_prime Int.prime_two] at h  exact h