如何利用实数域已证恒等式推导自然数域相同代数恒等式？

我已在实数域中证明了如下简单恒等式：

section
variable {P R q: ℝ}
theorem rq : R ^ 3 + q ^ 3 + P * R * q - R ^ 3 = q * (q ^ 2 + P * R) := by ring
end

现在我希望直接利用该实数域中的恒等式，证明自然数域上的完全相同的恒等式，不想通过改写对应定理的方式重复证明，因为这个过程比较繁琐。

内容的提问来源于stack exchange，提问作者DBE