no goals
R : Type u_1
S : Type ?u.77445
inst✝¹ : Ring R
inst✝ : Ring S
u : Rˣ
⊢ ↑(constantCoeff R) (invUnitsSub u) = 1 /ₚ u
rw [← coeff_zero_eq_constantCoeff_apply, coeff_invUnitsSub, zero_add, pow_one]