Theorem Set.diff_nonempty_of_ncard_lt_ncard

Modification history