Theorem Finset.exists_ne_of_one_lt_card

Modification history