feat(algebra/order/monoid_lemmas_zero_lt): add lemmas assuming mul_zero_class preorder (#13297)
mul_zero_class
preorder