Lemma grinvop (Y : gr) : ∏ y1 y2 : Y, (y1 * y2)^-1 = (y2^-1) * (y1^-1). Proof. intros y1 y2. apply (grrcan Y y1). rewrite (assocax Y). rewrite (grlinvax Y). rewrite (runax Y). apply (grrcan Y y2). rewrite (grlinvax Y). rewrite (assocax Y). rewrite (grlinvax Y). apply idpath. Qed.
Require Import UniMath.MoreFoundations.Subtypes.