no goals
R : Type u
S : Type v
k : Type y
A : Type z
a b : R
n : ℕ
inst✝ : DivisionRing R
p q : R[X]
h : p ≠ 0
⊢ Monic (p * ↑C (leadingCoeff p)⁻¹)
rw [Monic, leadingCoeff_mul, leadingCoeff_C,
  mul_inv_cancel (show leadingCoeff p ≠ 0 from mt leadingCoeff_eq_zero.1 h)]