Theorem Equiv.prodComm_symm

Modification history