Definition nat_nat_to_monoid_fun {X : gr} (x : X) : natset × natset -> X. Proof. intros n. exact (@op X (nat_to_monoid_fun x (dirprod_pr1 n)) (nat_to_monoid_fun (grinv X x) (dirprod_pr2 n))). Defined.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.