no goals
R : Type u
S : Type v
T : Type w
a b : R
n : ℕ
inst✝¹ : CommRing R
inst✝ : IsDomain R
p q : R[X]
hp1 : degree p = 1
hm : Monic p
⊢ p = X - ↑C (-coeff p 0)
simpa [hm.leadingCoeff] using eq_X_add_C_of_degree_eq_one hp1