Lemmas about ℤₘ₀.

theorem WithZero.ofAdd_zpow (a : ℤ) : ↑(Multiplicative.ofAdd a) = ↑(Multiplicative.ofAdd 1) ^ a

theorem WithZero.ofAdd_neg_one_pow_comm (a : ℤ) (n : ℕ) : (↑(Multiplicative.ofAdd (-1)) ^ (-a)) ^ n = ↑(Multiplicative.ofAdd ↑n) ^ a