R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
⊢ natDegree f + 1 ≤ n → 0 = coeff f (n * p)
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
⊢ coeff (contract p f) n = coeff f (n * p)
simp only [contract, coeff_monomial, sum_ite_eq', finset_sum_coeff, mem_range, not_lt,
  ite_eq_left_iff]
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : natDegree f + 1 ≤ n
⊢ 0 = coeff f (n * p)
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
⊢ natDegree f + 1 ≤ n → 0 = coeff f (n * p)
intro hn
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : natDegree f + 1 ≤ n
⊢ natDegree f < n * p
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : natDegree f + 1 ≤ n
⊢ 0 = coeff f (n * p)
apply (coeff_eq_zero_of_natDegree_lt _).symm
no goals
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : natDegree f + 1 ≤ n
⊢ natDegree f < n * p
calc
  f.natDegree < f.natDegree + 1 := Nat.lt_succ_self _
  _ ≤ n * 1 := by simpa only [mul_one] using hn
  _ ≤ n * p := mul_le_mul_of_nonneg_left (show 1 ≤ p from hp.bot_lt) (zero_le n)
no goals
R : Type u
inst✝¹ : CommSemiring R
S : Type v
inst✝ : CommSemiring S
p✝ q p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hn : natDegree f + 1 ≤ n
⊢ natDegree f + 1 ≤ n * 1
simpa only [mul_one] using hn