fact: Definition modulefun_to_binopfun : binopfun M N := make_binopfun pr1modulefun modulefun_to_isbinopfun.
imports: UniMath.MoreFoundations.Tactics UniMath.Algebra.RigsAndRings UniMath.Algebra.Groups UniMath.Algebra.Monoids