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