R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
this : degree (↑C a) < degree (X ^ n)
⊢ degree (X ^ n + ↑C a) = ↑n
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
⊢ degree (X ^ n + ↑C a) = ↑n
have : degree (C a) < degree ((X : R[X]) ^ n) :=
  degree_C_le.trans_lt <| by rwa [degree_X_pow, Nat.cast_withBot, WithBot.coe_pos]
no goals
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
this : degree (↑C a) < degree (X ^ n)
⊢ degree (X ^ n + ↑C a) = ↑n
rw [degree_add_eq_left_of_degree_lt this, degree_X_pow]
no goals
R : Type u
S : Type v
a✝ b c d : R
n✝ m : ℕ
inst✝¹ : Nontrivial R
inst✝ : Semiring R
n : ℕ
hn : 0 < n
a : R
⊢ 0 < degree (X ^ n)
rwa [degree_X_pow, Nat.cast_withBot, WithBot.coe_pos]