Lemma grtopathsxy (X : gr) {a b : X} (e : a * grinv X b = 1) : a = b . Proof. intros. set (e' := maponpaths (λ x, x * b) e). simpl in e'. rewrite (assocax X) in e'. rewrite (grlinvax X) in e'. rewrite (lunax X) in e'. rewrite (runax X) in e'. apply e'. Defined.
Require Import UniMath.Algebra.Groups.