Theorem Finset.insertNone_nonempty

Modification history