no goals
R : Type u_3
inst✝² : Semiring R
f : R[X]
S : Type u_1
F : Type u_2
inst✝¹ : Semiring S
inst✝ : AddMonoidHomClass F R[X] S[X]
φ : F
p : R[X]
φ_mon_nat : ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑φ (↑(monomial n) c)) = n
⊢ ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑φ (↑(monomial n) c)) = n - 0
simpa