feat(data/nat/factorial): additional inequalities (#6026)
feat(data/nat/factorial): additional inequalities (#6026)

I added two lemmas about factorials.  I use them in the Liouville PR #4301.





leanprover-community/mathlib,leanprover-community/mathlib