rw [totalDegree_add_eq_left_of_totalDegree_lt]
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
⊢ (X j ^ n + C r).totalDegree = n
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i j : ι
n : ℕ
hn : 0 < n
r : R
a✝ : Nontrivial R
⊢ (X j ^ n).totalDegree = n

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