feat(field_theory/ratfunc): add lemma `coe_sub` (#18542)
add lemma `coe_sub` stating that the coercion from rational functions to Laurent series commutes with subtraction. It is part of the long list of lemmas like `coe_add`, `coe_mul` and the like that were already there.
