Theorem vsub_vadd_comm

Modification history