Theorem Finset.Colex.singleton_lt_singleton

Modification history