feat(Algebra/Order/Archimedean/Submonoid): SubmonoidClass.instMulArchimedean (#16430)
SubmonoidClass.instMulArchimedean