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