mathlib

e763499b - chore(algebra/order/monoid_lemmas_zero_lt): remove redundant assumptions (#16524)