feat(data/nat/factorial): descending factorial (#7759)
- rename `desc_fac` to `asc_factorial`
- define `desc_factorial`
- update `data.fintype.card_embedding` to use `desc_factorial`
Co-authored-by: Eric <ericrboidi@gmail.com>
Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com>
