Positivity of the superfactorial

Nat.superFactorial n = 0! · 1! ⋯ n! is Mathlib's superfactorial, and Nat.prod_range_succ_factorial is its expansion as a product of factorials. Mathlib does not record the immediate consequence that the value is positive, which is what lets the superfactorial be cancelled from an identity over ℕ.

Main results

• TauCeti.Nat.superFactorial_pos: the superfactorial is positive.

theorem TauCeti.Nat.superFactorial_pos (n : ℕ) : 0 < n.superFactorial

The superfactorial is positive, being a product of factorials.