Lemma grinv_path_from_op_path {X : gr} {x y : X} (p : x * y = 1) : x^-1 = y. Proof. now rewrite <- (lunax X y), <- (grlinvax X x), assocax, p, runax. Defined.
Require Import UniMath.MoreFoundations.Subtypes.