fact: Definition ringofendabgr (G : abgr) : ring := @make_ring (setwith2binopofendabgr G) (@isringops_setofendabgr_op G).
imports: UniMath.MoreFoundations.Tactics UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.Monoids