fact: Definition subgrtosubmonoid (X : gr) : subgr X -> submonoid X := λ A : _, make_submonoid (pr1 A) (pr1 (pr2 A)).
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids