factorial): simpler proof of `mul_factorial_pred` (#5917)

Commit

4 years ago

refactor(data/nat/factorial): simpler proof of `mul_factorial_pred` (#5917) Co-authors: `lean-gptf`, Stanislas Polu

Author

Jesse Michael Han

Parents