proposition: Lemma isbinophrelgr (X : gr) {R : hrel X} (is : isinvbinophrel R) : isbinophrel R.
proof: Proof. set (is1 := pr1 is). set (is2 := pr2 is). split. - intros a b c r. rewrite (pathsinv0 (lunax X a)) in r. rewrite (pathsinv0 (lunax X b)) in r. rewrite (pathsinv0 (grlinvax X c)) in r. rewrite (assocax X _ _ a) in r. rewrite (assocax X _ _ b) in r. apply (is1 _ _ (grinv X c) r). - intros a b c r. rewrite (pathsinv0 (runax X a)) in r. rewrite (pathsinv0 (runax X b)) in r. rewrite (pathsinv0 (grrinvax X c)) in r. rewrite (pathsinv0 (assocax X a _ _)) in r. rewrite (pathsinv0 (assocax X b _ _)) in r. apply (is2 _ _ (grinv X c) r). Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids