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