fact: Definition rigmultsubmonoid {X : rig} : subrig X -> @submonoid (rigmultmonoid X) := λ A : _, @make_submonoid (rigmultmonoid X) (pr1 A) (pr2 (pr2 A)).
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids