refactor(algebra/*): small API fixes (#3157)
## Changes to `canonically_ordered_comm_semiring`
* in the definition of `canonically_ordered_comm_semiring` replace
`mul_eq_zero_iff` with `eq_zero_or_eq_zero_of_mul_eq_zero`; the other
implication is always true because of `[semiring]`;
* add instance `canonically_ordered_comm_semiring.to_no_zero_divisors`;
## Changes to `with_top`
* use `to_additive` for `with_top.has_one`, `with_top.coe_one` etc;
* move `with_top.coe_ne_zero` to `algebra.ordered_group`;
* add `with_top.has_add`, make `coe_add`, `coe_bit*` require only `[has_add α]`;
* use proper instances for lemmas about multiplication in `with_top`, not
just `canonically_ordered_comm_semiring` for everything;
## Changes to `associates`
* merge `associates.mk_zero_eq` and `associates.mk_eq_zero_iff_eq_zero` into
`associates.mk_eq_zero`;
* drop `associates.mul_zero`, `associates.zero_mul`, `associates.zero_ne_one`,
and `associates.mul_eq_zero_iff` in favor of typeclass instances;
## Misc changes
* drop `mul_eq_zero_iff_eq_zero_or_eq_zero` in favor of `mul_eq_zero`;
* drop `ennreal.mul_eq_zero` in favor of `mul_eq_zero` from instance.
