Theorem Ordinal.lt_mul_iff_of_isSuccLimit

Modification history