Theorem Set.encard_tsub_one_le_encard_diff_singleton

Modification history