Theorem Finset.Nontrivial.ne_singleton

Modification history