rw [totalDegree_add_eq_left_of_totalDegree_lt]
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
⊢ (X j + C r).totalDegree = 1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
⊢ (X j).totalDegree = 1

R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
r : R
a✝ : Nontrivial R
⊢ (C r).totalDegree < (X j).totalDegree