proposition: Lemma grtopathsxy (X : gr) {a b : X} (e : paths (op a (grinv X b)) (unel X) ) : a = b .
proof: Proof. intros. set (e' := maponpaths (λ x, op 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.
imports: UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings