mathlib3

b5c23cea - feat(data/nat/factorial): non-strict inequality on factorial (#6052)

feat(data/nat/factorial): non-strict inequality on factorial (#6052) Add lemmas add_factorial_le_factorial_add and add_factorial_le_factorial_add'. These are still used in the Liouville PR. I should have added them to the previous PR on factorials, but they got lost on the way!