Theorem Ordinal.card_eq_nat

Modification history