apply dvd_mul_right
F : Type
inst✝ : Field F
t p : Polynomial F
mt : t.Monic
⊢ t ∣ t * p

F : Type
inst✝ : Field F
t p : Polynomial F
mt : t.Monic
⊢ t.Monic
F : Type
inst✝ : Field F
t p : Polynomial F
mt : t.Monic
⊢ t.Monic