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