Theorem lt_max_of_lt_left

Modification history