R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬eval (↑(n - (ν - 1))) (pochhammer R ν) = 0
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ eval 0 ((↑derivative^[ν]) (bernsteinPolynomial R n ν)) ≠ 0
simp only [Int.coe_nat_eq_zero, bernsteinPolynomial.iterate_derivative_at_0, Ne.def,
  Nat.cast_eq_zero]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬↑(eval (n - (ν - 1)) (pochhammer ℕ ν)) = 0
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬eval (↑(n - (ν - 1))) (pochhammer R ν) = 0
simp only [← pochhammer_eval_cast]
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬eval (n - (ν - 1)) (pochhammer ℕ ν) = 0
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬↑(eval (n - (ν - 1)) (pochhammer ℕ ν)) = 0
norm_cast
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ 0 < eval (n - (ν - 1)) (pochhammer ℕ ν)
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ ¬eval (n - (ν - 1)) (pochhammer ℕ ν) = 0
apply ne_of_gt
case h.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n : ℕ
h : 0 ≤ n
⊢ 0 < eval (n - (0 - 1)) (pochhammer ℕ 0)

case h.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
h' : ν > 0
⊢ 0 < eval (n - (ν - 1)) (pochhammer ℕ ν)
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
⊢ 0 < eval (n - (ν - 1)) (pochhammer ℕ ν)
obtain rfl | h' := Nat.eq_zero_or_pos ν
no goals
case h.inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n : ℕ
h : 0 ≤ n
⊢ 0 < eval (n - (0 - 1)) (pochhammer ℕ 0)
simp
case h.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : Nat.succ (Nat.pred ν) ≤ n
h' : ν > 0
⊢ 0 < eval (n - (ν - 1)) (pochhammer ℕ ν)
case h.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : ν ≤ n
h' : ν > 0
⊢ 0 < eval (n - (ν - 1)) (pochhammer ℕ ν)
rw [← Nat.succ_pred_eq_of_pos h'] at h
no goals
case h.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharZero R
n ν : ℕ
h : Nat.succ (Nat.pred ν) ≤ n
h' : ν > 0
⊢ 0 < eval (n - (ν - 1)) (pochhammer ℕ ν)
exact pochhammer_pos _ _ (tsub_pos_of_lt (Nat.lt_of_succ_le h))