mathlib

64ad902d - refactor(algebra/order/{smul,module}): Turn lemmas around (#16696)

refactor(algebra/order/{smul,module}): Turn lemmas around (#16696) Match the `mul` lemmas by having the `⁻¹` on the LHS in `inv_smul_le_iff`, `inv_smul_lt_iff`, etc... Also generalize for free to `ordered_add_comm_monoid`.