fact: Definition moduletomonoid {R : ring} (M : module R) : abmonoid := abgrtoabmonoid (pr1module M).
imports: UniMath.MoreFoundations.Tactics UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.Monoids