R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬eval (Nat.succ ν) (pochhammer ℕ (n - ν)) = 0
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ eval 1 ((↑derivative^[n - ν]) (bernsteinPolynomial R n ν)) ≠ 0
rw [bernsteinPolynomial.iterate_derivative_at_1 _ _ _ h, Ne.def, neg_one_pow_mul_eq_zero_iff, ←
  Nat.cast_succ, ← pochhammer_eval_cast, ← Nat.cast_zero, Nat.cast_inj]
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬eval (Nat.succ ν) (pochhammer ℕ (n - ν)) = 0
exact (pochhammer_pos _ _ (Nat.succ_pos ν)).ne'