Theorem Ordinal.nat_lt_limit

Modification history