fact: Definition make_issubgr {X : gr} {A : hsubtype X} (H1 : issubmonoid A) (H2 : ∏ x : X, A x -> A (grinv X x)) : issubgr A := make_dirprod H1 H2.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids