refactor(data/nat/choose): reduce assumptions on lemmas (#8508)
- rename `nat.choose_eq_factorial_div_factorial'` to `nat.cast_choose`
- change the cast from `ℚ` to any `char_zero` field
- get rid of the cast in `nat.choose_mul`. Generalization ensues.
