Commit 2023-10-26 21:10 c38470f3

feat: port positivity extension for Nat.ascFactorial (#7931) Adds a positivity extension for Nat.ascFactorial. (Compare to the lean 3 version: https://github.com/leanprover-community/mathlib/blob/3365b20c2ffa7c35e47e5209b89ba9abdddf3ffe/src/tactic/positivity.lean#L762-L767) Also updates the Nat.factorial positivity extension to use a more idiomatic ~q() match.