no goals
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
⊢ degree (↑C a * T n) = if a = 0 then ⊥ else ↑n
split_ifs with h <;>
  simp only [h, map_zero, MulZeroClass.zero_mul, degree_zero, degree_C_mul_T, Ne.def,
    not_false_iff]