feat(algebra/*/opposite): Missing instances (#18602)
A few missing instances about `nat.cast`/`int.cast`/`rat.cast` and `mul_opposite`/`add_opposite`.
Also add the (weirdly) missing `add_comm_group_with_one → add_comm_monoid_with_one`.
Finally, this changes the defeq of `rat.cast` on `mul_opposite` to be simpler.
