Definition rinvpairxy (X : monoid) (x y : X) (x' : rinvpair X x) (y' : rinvpair X y) : rinvpair X (x * y). Proof. intros. exists (pr1 y' * pr1 x'). rewrite (assocax _ x y _). rewrite <- (assocax _ y _ _). rewrite (pr2 y'). rewrite (lunax _ _). rewrite (pr2 x'). apply idpath. Defined.
Require Import UniMath.Algebra.Groups.