case a.zero
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.469754
h : degree p ≤ 0
⊢ coeff p Nat.zero = coeff (↑C (coeff p 0)) Nat.zero

case a.succ
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.469754
h : degree p ≤ 0
n : ℕ
⊢ coeff p (Nat.succ n) = coeff (↑C (coeff p 0)) (Nat.succ n)
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.469754
h : degree p ≤ 0
⊢ p = ↑C (coeff p 0)
ext (_ | n)
case a.succ
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.469754
h : degree p ≤ 0
n : ℕ
⊢ degree p < ↑(Nat.succ n)
case a.succ
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.469754
h : degree p ≤ 0
n : ℕ
⊢ coeff p (Nat.succ n) = coeff (↑C (coeff p 0)) (Nat.succ n)
rw [coeff_C, if_neg (Nat.succ_ne_zero _), coeff_eq_zero_of_degree_lt]
no goals
case a.succ
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.469754
h : degree p ≤ 0
n : ℕ
⊢ degree p < ↑(Nat.succ n)
exact h.trans_lt (WithBot.some_lt_some.2 n.succ_pos)
no goals
case a.zero
R : Type u
S : Type v
a b c d : R
n m : ℕ
inst✝ : Semiring R
p q : R[X]
ι : Type ?u.469754
h : degree p ≤ 0
⊢ coeff p Nat.zero = coeff (↑C (coeff p 0)) Nat.zero
simp