Theorem max_left_comm

Modification history