no goals
R : Type u_1
S : Type ?u.286917
F : Type ?u.286920
K : Type ?u.286923
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
h : toPoly P = toPoly Q
⊢ P.c = Q.c
rw [← coeff_eq_c, h, coeff_eq_c]