chore(*): fix docs and a name generated by to_additive (#18002)
The autogenerated name was `order_of_add_eq_right_of_forall_prime_add_dvd`, but the second `add` shouldn't be to_additivized. Now corrected to `add_order_of_add_eq_right_of_forall_prime_mul_dvd`. I've checked the namespace still gets correctly additivized to `add_commute`.
Co-authored-by: Oliver Nash <github@olivernash.org>
Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
