Theorem Ordinal.one_lt_card

Modification history