for L being non trivial right_unital associative doubleLoopStr
for a, b being Element of L st b is left_invertible & b is right_mult-cancelable & b * (/ b) = (/ b) * b holds
(a * b) / b = a