Theorem Ordinal.natCast_lt_omega0

Modification history