no goals
R : Type u_1
S : Type ?u.551311
F : Type ?u.551314
K : Type ?u.551317
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
hd : P.d = 0
⊢ toPoly P = 0
rw [of_c_eq_zero ha hb hc, hd, C_0]