no goals
R : Type u_1
S : Type ?u.580862
F : Type ?u.580865
K : Type ?u.580868
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
⊢ degree (toPoly P) ≤ 1
simpa only [of_b_eq_zero ha hb] using degree_linear_le