Lemma isinvbinophrelgr (X : gr) {R : hrel X} (is : isbinophrel R) : isinvbinophrel R. Proof. set (is1 := pr1 is). set (is2 := pr2 is). split. - intros a b c r. set (r' := is1 _ _ (c^-1) r). clearbody r'. rewrite <- (assocax X _ _ a) in r'. rewrite <- (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 _ _ (c^-1) 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'. Qed.
Require Import UniMath.MoreFoundations.Subtypes.