Theorem Ordinal.card_lt_ofNat

Modification history