Commit 2022-09-14 18:51 660bde43

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.