case h.e'_3.h₁.a
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ n = 0 ↔ 0 = n
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ coeff (↑C a) n = if n = 0 then a else 0
convert coeff_monomial (a := a) (m := n) (n := 0) using 2
no goals
case h.e'_3.h₁.a
R : Type u
a b : R
m n : ℕ
inst✝ : Semiring R
p q : R[X]
⊢ n = 0 ↔ 0 = n
simp [eq_comm]