Theorem Max.left_comm

Modification history