no goals
R : Type u
S : Type v
a b : R
n m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
k m : ℕ
h : k ≠ m
x y : R
hx : x ≠ 0
hy : y ≠ 0
⊢ card (support (↑C x * X ^ k + ↑C y * X ^ m)) = 2
rw [support_binomial h hx hy, card_insert_of_not_mem (mt mem_singleton.mp h), card_singleton]