∀ {R : Type u} {a b c d : R} [inst : Semiring R],
  a ≠ 0 →
    (Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X + Polynomial.C d).degree <
      (Polynomial.C a * Polynomial.X ^ 3).degree