feat(algebra/order/monoid): add `le_iff_exists_mul'` (#14387)
feat(algebra/order/monoid): add `le_iff_exists_mul'` (#14387)

Add a version of `le_iff_exists_mul'`/`le_iff_exists_add'`, versions of `le_iff_exists_mul`/`le_iff_exists_add` with multiplication on the other side.





leanprover-community/mathlib,leanprover-community/mathlib