no goals
R : Type u
S : Type v
a b : R
m n✝ : ℕ
ι : Type y
inst✝ : Ring R
p : R[X]
n : ℕ
H : degree p ≤ ↑n
⊢ Monic (X ^ (n + 1) - p)
simpa [sub_eq_add_neg] using monic_X_pow_add (show degree (-p) ≤ n by rwa [← degree_neg p] at H)
no goals
R : Type u
S : Type v
a b : R
m n✝ : ℕ
ι : Type y
inst✝ : Ring R
p : R[X]
n : ℕ
H : degree p ≤ ↑n
⊢ degree (-p) ≤ ↑n
rwa [← degree_neg p] at H