Theorem IsOrderedMonoid.ofSubmonoid

Modification history