case pos
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
r : R
hn : n = 0
⊢ natDegree (X ^ n + ↑C r) = n

case neg
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
r : R
hn : ¬n = 0
⊢ natDegree (X ^ n + ↑C r) = n
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
r : R
⊢ natDegree (X ^ n + ↑C r) = n
by_cases hn : n = 0
no goals
case pos
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
r : R
hn : n = 0
⊢ natDegree (X ^ n + ↑C r) = n
rw [hn, pow_zero, ← C_1, ← RingHom.map_add, natDegree_C]
no goals
case neg
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
r : R
hn : ¬n = 0
⊢ natDegree (X ^ n + ↑C r) = n
exact natDegree_eq_of_degree_eq_some (degree_X_pow_add_C (pos_iff_ne_zero.mpr hn) r)