no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.1327898
ha : a ≠ 0
⊢ degree (↑C b * X ^ 2 + ↑C c * X + ↑C d) < degree (↑C a * X ^ 3)
simpa only [degree_C_mul_X_pow 3 ha] using degree_quadratic_lt