R : Type u
S : Type v
a b : R
n✝ m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ {k, m, n} ⊆ support (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)
R : Type u
S : Type v
a b : R
n✝ m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ support (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n) = {k, m, n}
apply subset_antisymm (support_trinomial' k m n x y z)
no goals
R : Type u
S : Type v
a b : R
n✝ m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
k m n : ℕ
hkm : k < m
hmn : m < n
x y z : R
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ {k, m, n} ⊆ support (↑C x * X ^ k + ↑C y * X ^ m + ↑C z * X ^ n)
simp_rw [insert_subset, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul,
  coeff_X_pow_self, mul_one, coeff_X_pow, if_neg hkm.ne, if_neg hkm.ne', if_neg hmn.ne,
  if_neg hmn.ne', if_neg (hkm.trans hmn).ne, if_neg (hkm.trans hmn).ne', mul_zero, add_zero,
  zero_add, Ne.def, hx, hy, hz]