refactor(algebra/order/monoid_lemma_zero_lt): Use {x : α // 0 ≤ α} (#16447)

`pos_mul_mono`/`mul_pos_mono` and `pos_mul_reflect_lt`/`mul_pos_reflect_lt` were stated as covariance/contravariance of `{x : α // 0 < α}` over `α` even though the extension to `{x : α // 0 ≤ α}` also holds.

This meant that many lemmas were relying on antisymmetry only to treat the cases `a = 0` and `0 < a` separately, which made them need `partial_order` and depend on `classical.choice`. This prevented #16172 from actually removing the `decidable` lemma in `algebra.order.ring` after #16189 got merged.

Further, #16189 did not actually get rid of the temporary `zero_lt` namespace, so name conflicts that arise were not fixed.

Finally, `le_mul_of_one_le_left` and its seven friends were reproved inline about five time each.

Hence in this PR we
* restate `pos_mul_mono`, `mul_pos_mono`, `pos_mul_reflect_lt`, `mul_pos_reflect_lt` using `{x : α // 0 ≤ α}`
* provide the (classical) equivalence with the previous definitions in a `partial_order`.
* generalise lemmas from `partial_order` to `preorder`.
* delete all lemmas in the `preorder` namespace as they are now fully generalized. This in essence reverts (parts of) #12961, #13296 and #13299.
* replace most of the various `has_le`/`has_lt` assumptions by a blank `preorder` one, hence simplifying the file sectioning
* remove the `zero_lt` namespace.
* rename lemmas to fix name conflicts.
* delete a few lemmas that were left in `algebra.order.ring`.
* golf proofs involving `le_mul_of_one_le_left` and its seven friends. This is why the PR has a -450 lines diff.

Author: YaelDillies