no goals
R : Type u_1
S : Type ?u.555902
F : Type ?u.555905
K : Type ?u.555908
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b ≠ 0
⊢ leadingCoeff (toPoly P) = P.b
rw [of_a_eq_zero ha, leadingCoeff_quadratic hb]