Theorem inv_lt_of_inv_lt

Modification history