Definition rcanfromrinv (X : monoid) (a b c : X) (c' : rinvpair X c) (e : a * c = b * c) : a = b. Proof. intros. set (e' := maponpaths (λ x : X, x * (pr1 c')) e). simpl in e'. rewrite (assocax X _ _ _) in e'. rewrite (assocax X _ _ _) in e'. rewrite (pr2 c') in e'. rewrite (runax X a) in e'. rewrite (runax X b) in e'. apply e'. Defined.
Require Import UniMath.Algebra.Groups.