mathlib3

f51fe7b6 - chore(data/fin): Improve docstrings, rename `coe_sub_nat`, add `nat_add_zero` (#5290)

chore(data/fin): Improve docstrings, rename `coe_sub_nat`, add `nat_add_zero` (#5290) These are cherry-picked from the tuple PR, #4406. `coe_sub_nat` was previously named `sub_nat_coe`, but this didn't match `coe_nat_add` and `coe_add_nat`.