Theorem invOf_two_smul_add_invOf_two_smul

Modification history