Theorem mul_inv_lt_iff

Modification history