proposition: Lemma grquotinvcomp {X : gr} (R : binopeqrel X) : iscomprelrelfun R R (grinv X).
proof: Proof. destruct R as [ R isb ]. set (isc := iscompbinoptransrel _ (eqreltrans _) isb). unfold iscomprelrelfun. intros x x' r. destruct R as [ R iseq ]. destruct iseq as [ ispo0 symm0 ]. destruct ispo0 as [ trans0 refl0 ]. unfold isbinophrel in isb. set (r0 := isc _ _ _ _ (isc _ _ _ _ (refl0 (grinv X x')) r) (refl0 (grinv X x))). rewrite (grlinvax X x') in r0. rewrite (assocax X (grinv X x') x (grinv X x)) in r0. rewrite (grrinvax X x) in r0. rewrite (lunax X _) in r0. rewrite (runax X _) in r0. apply (symm0 _ _ r0). Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids