feat(algebra/group_with_zero): mul_self_mul_inv (#2795)
I found this lemma was useful for simplifying some expressions without
needing to split into cases or provide a proof that the denominator is
nonzero, and it doesn't show up with library_search.
