case zero
S : Type u_1
inst✝ : StrictOrderedSemiring S
s : S
h : 0 < s
⊢ 0 < eval s (pochhammer S Nat.zero)

case succ
S : Type u_1
inst✝ : StrictOrderedSemiring S
s : S
h : 0 < s
n : ℕ
ih : 0 < eval s (pochhammer S n)
⊢ 0 < eval s (pochhammer S (Nat.succ n))
S : Type u_1
inst✝ : StrictOrderedSemiring S
n : ℕ
s : S
h : 0 < s
⊢ 0 < eval s (pochhammer S n)
induction' n with n ih
case zero
S : Type u_1
inst✝ : StrictOrderedSemiring S
s : S
h : 0 < s
⊢ 0 < 1
case zero
S : Type u_1
inst✝ : StrictOrderedSemiring S
s : S
h : 0 < s
⊢ 0 < eval s (pochhammer S Nat.zero)
simp only [Nat.zero_eq, pochhammer_zero, eval_one]
no goals
case zero
S : Type u_1
inst✝ : StrictOrderedSemiring S
s : S
h : 0 < s
⊢ 0 < 1
exact zero_lt_one
case succ
S : Type u_1
inst✝ : StrictOrderedSemiring S
s : S
h : 0 < s
n : ℕ
ih : 0 < eval s (pochhammer S n)
⊢ 0 < eval s (pochhammer S n) * (s + ↑n)
case succ
S : Type u_1
inst✝ : StrictOrderedSemiring S
s : S
h : 0 < s
n : ℕ
ih : 0 < eval s (pochhammer S n)
⊢ 0 < eval s (pochhammer S (Nat.succ n))
rw [pochhammer_succ_right, mul_add, eval_add, ← Nat.cast_comm, eval_nat_cast_mul, eval_mul_X,
  Nat.cast_comm, ← mul_add]
no goals
case succ
S : Type u_1
inst✝ : StrictOrderedSemiring S
s : S
h : 0 < s
n : ℕ
ih : 0 < eval s (pochhammer S n)
⊢ 0 < eval s (pochhammer S n) * (s + ↑n)
exact mul_pos ih (lt_of_lt_of_le h ((le_add_iff_nonneg_right _).mpr (Nat.cast_nonneg n)))