∀ {R : Type u} [inst : Semiring R] {k m n : ℕ},
  k < m →
    m < n →
      ∀ {x y z : R},
        x ≠ 0 →
          y ≠ 0 →
            z ≠ 0 →
              (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m +
                      Polynomial.C z * Polynomial.X ^ n).support.card =
                3