feat(data/rat/basic): Add nat num and denom inv lemmas (#8581)
Add `inv_coe_nat_num` and `inv_coe_nat_denom` lemmas.
These lemmas show that the denominator and numerator of `1/ n` given `0 < n`, are equal to `n` and `1` respectively.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
