no goals
R : Type u
inst✝ : CommRing R
hdomain : IsDomain R
r s : R
p q : R[X]
f x✝¹ x✝ : RatFunc R
h : ↑(laurent r) x✝¹ = ↑(laurent r) x✝
⊢ x✝¹ = x✝
simpa [laurent_laurent] using congr_arg (laurent (-r)) h