no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.936788
⊢ degree (↑C a * X ^ 2 + ↑C b * X + ↑C c) ≤ 2
simpa only [add_assoc] using
  degree_add_le_of_degree_le (degree_C_mul_X_pow_le 2 a)
    (le_trans degree_linear_le <| WithBot.coe_le_coe.mpr one_le_two)