Lemma grquotinvcomp {X : gr} (R : binopeqrel X) : iscomprelrelfun R R (λ x, x^-1). Proof. induction R as [ R isb ]. set (isc := iscompbinoptransrel _ (eqreltrans _) isb). unfold iscomprelrelfun. intros x x' r. induction R as [ R iseq ]. induction iseq as [ ispo0 symm0 ]. induction ispo0 as [ trans0 refl0 ]. unfold isbinophrel in isb. set (r0 := isc _ _ _ _ (isc _ _ _ _ (refl0 (x'^-1)) r) (refl0 (x^-1))). rewrite (grlinvax X x') in r0. rewrite (assocax X (x'^-1) x (x^-1)) in r0. rewrite (grrinvax X x) in r0. rewrite (lunax X _) in r0. rewrite (runax X _) in r0. apply (symm0 _ _ r0). Qed.
Require Import UniMath.MoreFoundations.Subtypes.