proposition: Lemma isabgrcarrier {X : abgr} (A : subgr X) : isabgrop (@op A).
proof: Proof. split with (isgrcarrier A). apply (pr2 (@isabmonoidcarrier X A)). Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids