Theorem ENat.card_le_one_iff_subsingleton

Modification history