Theorem mul_invOf_cancel_left

Modification history