Theorem Ordinal.mul_le_iff_of_isSuccLimit

Modification history