no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.668511
h : card (support p) ≤ 1
⊢ ↑C (leadingCoeff p) * X ^ natDegree p = p
rw [C_mul_X_pow_eq_monomial, monomial_natDegree_leadingCoeff_eq_self h]