English
For any n and s with n − 1 ≤ s in a strictly ordered ring S, the evaluation (descPochhammer S n).eval s is nonnegative.
Русский
Для любых n и s в строго упорядоченном кольце S, при n − 1 ≤ s, значение (descPochhammer S n).eval s неотрицательно.
LaTeX
$$$\\text{If } n \\in \\mathbb{N},\\ s \\in S,\\ n-1 \\le s \\Rightarrow 0 \\le (\\operatorname{descPochhammer} \\, S\\, n).\\mathrm{eval}\\, s$.$$
Lean4
/-- `descPochhammer S n` is nonnegative on `[n-1, ∞)`. -/
theorem descPochhammer_nonneg {n : ℕ} {s : S} (h : n - 1 ≤ s) : 0 ≤ (descPochhammer S n).eval s :=
by
rcases eq_or_lt_of_le h with heq | h
· rw [← heq, descPochhammer_eval_eq_ascPochhammer, sub_sub_cancel_left, neg_add_cancel, ascPochhammer_eval_zero]
positivity
· exact (descPochhammer_pos h).le
