no goals
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.910503
ha : a ≠ 0
⊢ leadingCoeff (↑C a * X + ↑C b) = a
rw [add_comm, leadingCoeff_add_of_degree_lt (degree_C_lt_degree_C_mul_X ha),
  leadingCoeff_C_mul_X]