proposition: Lemma grfromgtunel (X : gr) {R : hrel X} (is : isbinophrel R) {x : X} (isg : R x (unel X)) : R (unel X) (grinv X x).
proof: Proof. intros. set (r := (pr2 is) _ _ (grinv X x) isg). rewrite (grrinvax X x) in r. rewrite (lunax X _) in r. apply r. Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids