no goals
R : Type u_1
S : Type ?u.587971
F : Type ?u.587974
K : Type ?u.587977
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
⊢ natDegree (toPoly P) ≤ 2
simpa only [of_a_eq_zero ha] using natDegree_quadratic_le