mathlib3

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

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.