no goals
R : Type u
S : Type v
a b c d : R
n✝ m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : degree p ≤ 1
n : ℕ
⊢ coeff p Nat.zero = coeff (↑C (coeff p 1) * X + ↑C (coeff p 0)) Nat.zero
simp
no goals
R : Type u
S : Type v
a b c d : R
n✝¹ m : ℕ
inst✝ : Semiring R
p q r : R[X]
h : degree p ≤ 1
n✝ n : ℕ
⊢ coeff p (Nat.succ Nat.zero) = coeff (↑C (coeff p 1) * X + ↑C (coeff p 0)) (Nat.succ Nat.zero)
simp [coeff_C]
R : Type u
S : Type v
a b c d : R
n✝¹ m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
h : degree p ≤ 1
n✝ n m : ℕ
this : degree p < ↑(Nat.succ (Nat.succ m))
⊢ coeff p (Nat.succ (Nat.succ m)) = coeff (↑C (coeff p 1) * X + ↑C (coeff p 0)) (Nat.succ (Nat.succ m))
R : Type u
S : Type v
a b c d : R
n✝¹ m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
h : degree p ≤ 1
n✝ n m : ℕ
⊢ coeff p (Nat.succ (Nat.succ m)) = coeff (↑C (coeff p 1) * X + ↑C (coeff p 0)) (Nat.succ (Nat.succ m))
have : degree p < m.succ.succ := lt_of_le_of_lt h
  (Iff.mpr WithBot.coe_lt_coe <| Nat.succ_lt_succ <| Nat.zero_lt_succ m)
no goals
R : Type u
S : Type v
a b c d : R
n✝¹ m✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
h : degree p ≤ 1
n✝ n m : ℕ
this : degree p < ↑(Nat.succ (Nat.succ m))
⊢ coeff p (Nat.succ (Nat.succ m)) = coeff (↑C (coeff p 1) * X + ↑C (coeff p 0)) (Nat.succ (Nat.succ m))
simp [coeff_eq_zero_of_degree_lt this, coeff_C, Nat.succ_ne_zero, coeff_X, Nat.succ_inj',
  @eq_comm ℕ 0]