R : Type u
S : Type v
a b : R
n m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ {k, m} ⊆ support (↑C x * X ^ k + ↑C y * X ^ m)
R : Type u
S : Type v
a b : R
n m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ support (↑C x * X ^ k + ↑C y * X ^ m) = {k, m}
apply subset_antisymm (support_binomial' k m x y)
no goals
R : Type u
S : Type v
a b : R
n m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
k m : ℕ
hkm : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ {k, m} ⊆ support (↑C x * X ^ k + ↑C y * X ^ m)
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, if_neg hkm.symm, mul_zero, zero_add,
  add_zero, Ne.def, hx, hy]