Definition invpairxy (X : monoid) (x y : X) (x' : invpair X x) (y' : invpair X y) : invpair X (x * y). Proof. intros. exists (pr1 y' * pr1 x'). split. - apply (pr2 (linvpairxy _ x y (invtolinv _ x x') (invtolinv _ y y'))). - apply (pr2 (rinvpairxy _ x y (invtorinv _ x x') (invtorinv _ y y'))). Defined.
Require Import UniMath.Algebra.Groups.