R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝¹ : Nontrivial R
inst✝ : Semiring R
a : R
this : degree (↑C a) < degree X
⊢ degree (X + ↑C a) = 1
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝¹ : Nontrivial R
inst✝ : Semiring R
a : R
⊢ degree (X + ↑C a) = 1
have : degree (C a) < degree (X : R[X]) :=
  calc
    degree (C a) ≤ 0 := degree_C_le
    _ < 1 := (WithBot.some_lt_some.mpr zero_lt_one)
    _ = degree X := degree_X.symm
no goals
R : Type u
S : Type v
a✝ b c d : R
n m : ℕ
inst✝¹ : Nontrivial R
inst✝ : Semiring R
a : R
this : degree (↑C a) < degree X
⊢ degree (X + ↑C a) = 1
rw [degree_add_eq_left_of_degree_lt this, degree_X]