case inl
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
I : Decidable (n < 1 + natDegree p)
h : n < 1 + natDegree p
⊢ coeff p n = coeff p n

case inr
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
I : Decidable (n < 1 + natDegree p)
h : ¬n < 1 + natDegree p
⊢ 0 = coeff p n
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
I : Decidable (n < 1 + natDegree p)
⊢ (if n < 1 + natDegree p then coeff p n else 0) = coeff p n
split_ifs with h
no goals
case inl
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
I : Decidable (n < 1 + natDegree p)
h : n < 1 + natDegree p
⊢ coeff p n = coeff p n
rfl
no goals
case inr
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p✝ q r p : R[X]
n : ℕ
I : Decidable (n < 1 + natDegree p)
h : ¬n < 1 + natDegree p
⊢ 0 = coeff p n
exact (coeff_eq_zero_of_natDegree_lt (not_le.1 fun w => h (Nat.lt_one_add_iff.2 w))).symm