Theorem Ordinal.le_succ_of_isLimit

Modification history