feat(algebra/module): `sub_mem_iff_left` and `sub_mem_iff_right` (#13043)
feat(algebra/module): `sub_mem_iff_left` and `sub_mem_iff_right` (#13043)

Since it's a bit of a hassle to rewrite `add_mem_iff_left` and `add_mem_iff_right` to subtraction, I made a new pair of lemmas.





leanprover-community/mathlib,leanprover-community/mathlib