Theorem AddOpposite.op_mul

Modification history