mathlib3

ba998da9 - feat(algebra/order/monoid_lemmas_zero_lt): more lemmas using `pos_mul` and friends (#12355)

feat(algebra/order/monoid_lemmas_zero_lt): more lemmas using `pos_mul` and friends (#12355) This PR continues the `order` refactor. The added lemmas are the `\le` analogues of the `<` lemmas that are already present.