Psi summand coeff eq zero of ne mod

theorem psi_summand_coeff_eq_zero_of_ne_mod (α κ : ℕ) (h2 : (2 : ZMod q) ≠ 0)    (hk : 2 * 2 ^ κ ∣ 2 ^ α) (a : Fin (2 ^ α / 2 ^ κ) → fixedSubring (R := ZMod q) α (2 ^ κ))    {p : ℕ} (hp : p < 2 ^ α) (j : Fin (2 ^ α / 2 ^ κ))    (hne : p % 2 ^ (α - κ - 1) ≠ (j : ℕ) % 2 ^ (α - κ - 1)) :    ((a j : Rq (powTwoCyclotomic (R := ZMod q) α))      * Xpow (powTwoCyclotomic α) (packExp α (2 ^ κ) (j : ℕ))).1.coeff p = 0 := by  have hκ : κ + 1 ≤ α := succ_le_of_two_mul_two_pow_dvd hk  rw [Xpow_mul_coeff α (packExp α (2 ^ κ) (j : ℕ)) (packExp_lt α κ hk j)    (a j : Rq (powTwoCyclotomic (R := ZMod q) α)) hp]  split_ifs with hle  · apply fixedSubring_coeff_eq_zero q α κ h2 hk (a j) (by omega)    intro hdvd    apply hne    have hmeq : packExp α (2 ^ κ) (j : ℕ) % 2 ^ (α - κ - 1) = p % 2 ^ (α - κ - 1) :=      (Nat.modEq_iff_dvd' hle).mpr hdvd    rw [packExp_mod_eq α κ hk j] at hmeq; omega  · rw [fixedSubring_coeff_eq_zero q α κ h2 hk (a j) (by omega) (by      intro hdvd      apply hne      have hle2 : packExp α (2 ^ κ) (j : ℕ) ≤ p + 2 ^ α := by        have := packExp_lt α κ hk j; omega      have hmeq : packExp α (2 ^ κ) (j : ℕ) % 2 ^ (α - κ - 1)          = (p + 2 ^ α) % 2 ^ (α - κ - 1) := (Nat.modEq_iff_dvd' hle2).mpr hdvd      have h2z : (2 : ℕ) ^ α % 2 ^ (α - κ - 1) = 0 := by        rw [show (2 : ℕ) ^ α = 2 ^ (α - κ - 1) * 2 ^ (κ + 1) from by          rw [← pow_add]; congr 1; omega, Nat.mul_mod_right]      rw [packExp_mod_eq α κ hk j, Nat.add_mod, h2z, Nat.add_zero, Nat.mod_mod] at hmeq      omega),      neg_zero]