Theorem Finset.card_add_card_sub_one_le_card_mul

Modification history