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