proposition: Lemma pathslinvtorinv (X : monoid) (x : X) (x' : linvpair X x) (x'' : rinvpair X x) : paths (pr1 x') (pr1 x'').
proof: Proof. intros. destruct (runax X (pr1 x')). destruct (pr2 x''). set (int := x * pr1 x''). rewrite <- (lunax X (pr1 x'')). destruct (pr2 x'). unfold int. apply (pathsinv0 (assocax X _ _ _)). Defined.
imports: UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings