Theorem mul_right_cancel''

Modification history