Lemma isbinophrelgr (X : gr) {R : hrel X} (is : isinvbinophrel R) : isbinophrel R. Proof. set (is1 := pr1 is). set (is2 := pr2 is). split. - intros a b c r. rewrite <- (lunax X a) in r. rewrite <- (lunax X b) in r. rewrite <- (grlinvax X c) in r. rewrite (assocax X _ _ a) in r. rewrite (assocax X _ _ b) in r. apply (is1 _ _ (c^-1) r). - intros a b c r. rewrite <- (runax X a) in r. rewrite <- (runax X b) in r. rewrite <- (grrinvax X c) in r. rewrite <- (assocax X a _ _) in r. rewrite <- (assocax X b _ _) in r. apply (is2 _ _ (c^-1) r). Qed.
Require Import UniMath.MoreFoundations.Subtypes.