Theorem lt_of_mul_self_lt_mul_self

Modification history