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]
k : ℕ
φ_k : ∀ (f : R[X]), natDegree f < k → ↑φ f = 0
φ_mon : ∀ (n : ℕ) (c : R), c ≠ 0 → natDegree (↑φ (↑(monomial n) c)) = n - k
⊢ ∀ {n : ℕ}, n ≤ k → (fun j => j - k) n = 0
simp