Lemma pathslinvtorinv (X : monoid) (x : X) (x' : linvpair X x) (x'' : rinvpair X x) : pr1 x' = pr1 x''. Proof. intros. induction (runax X (pr1 x')). induction (pr2 x''). set (int := x * pr1 x''). rewrite <- (lunax X (pr1 x'')). induction (pr2 x'). unfold int. apply (!assocax X _ _ _). Defined.
Require Import UniMath.Algebra.Groups.