Nonvanishing factorials

The factorial of a natural number is nonzero. Registering this fact as an instance also lets NeZero.charZero infer nonvanishing of factorials cast to characteristic-zero scalars, so constructions requiring an invertible factorial apply automatically there.

The file also records Nat.sq_eq_descFactorial_two_add, the expansion n ^ 2 = (n)₂ + n of a square into falling factorials, which converts second factorial moments into second moments, and Nat.six_pow_mul_factorial_le_factorial_two_mul_add_one, 6 ^ n * n ! ≤ (2 * n + 1)!, the termwise comparison of the power series of x * exp (x ^ 2 / 6) and sinh x.

instance TauCeti.instNeZeroFactorial {n : ℕ} : NeZero n.factorial

Natural factorials are nonzero, also enabling automatic nonvanishing of their casts to characteristic-zero scalars.

theorem Nat.sq_eq_descFactorial_two_add (n : ℕ) : n ^ 2 = n.descFactorial 2 + n

A square is the second falling factorial plus the number itself: n ^ 2 = (n)₂ + n.

theorem Nat.six_pow_mul_factorial_le_factorial_two_mul_add_one (n : ℕ) : 6 ^ n * n.factorial ≤ (2 * n + 1).factorial

6 ^ n * n ! ≤ (2 * n + 1)!, with equality at n = 0 and n = 1.