case pos
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a = 0
⊢ degree (↑C a * T n) ≤ ↑n

case neg
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : ¬a = 0
⊢ degree (↑C a * T n) ≤ ↑n
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
⊢ degree (↑C a * T n) ≤ ↑n
by_cases a0 : a = 0
no goals
case pos
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a = 0
⊢ degree (↑C a * T n) ≤ ↑n
simp only [a0, map_zero, MulZeroClass.zero_mul, degree_zero, bot_le]
no goals
case neg
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : ¬a = 0
⊢ degree (↑C a * T n) ≤ ↑n
exact (degree_C_mul_T n a a0).le