Theorem Right.mul_lt_one_of_le_of_lt

Modification history