case intro
R✝ : Type u
S : Type v
a✝ b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Ring R✝
p : R✝[X]
R : Type u
inst✝ : Ring R
a : R
k : ℕ
h : Nat.succ k ≠ 0
⊢ Monic (X ^ Nat.succ k - ↑C a)
R✝ : Type u
S : Type v
a✝ b : R✝
m n✝ : ℕ
ι : Type y
inst✝¹ : Ring R✝
p : R✝[X]
R : Type u
inst✝ : Ring R
a : R
n : ℕ
h : n ≠ 0
⊢ Monic (X ^ n - ↑C a)
obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h
R✝ : Type u
S : Type v
a✝ b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Ring R✝
p : R✝[X]
R : Type u
inst✝ : Ring R
a : R
k : ℕ
h : Nat.succ k ≠ 0
⊢ degree (↑C a) ≤ ↑k
case intro
R✝ : Type u
S : Type v
a✝ b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Ring R✝
p : R✝[X]
R : Type u
inst✝ : Ring R
a : R
k : ℕ
h : Nat.succ k ≠ 0
⊢ Monic (X ^ Nat.succ k - ↑C a)
apply monic_X_pow_sub _
no goals
R✝ : Type u
S : Type v
a✝ b : R✝
m n : ℕ
ι : Type y
inst✝¹ : Ring R✝
p : R✝[X]
R : Type u
inst✝ : Ring R
a : R
k : ℕ
h : Nat.succ k ≠ 0
⊢ degree (↑C a) ≤ ↑k
exact le_trans degree_C_le Nat.WithBot.coe_nonneg