proposition: Lemma grinv_path_from_op_path {X : gr} {x y : X} (p : (x * y)%multmonoid = unel X) : grinv X x = y.
proof: Proof. now rewrite <- (lunax X y), <- (grlinvax X x), assocax, p, runax. Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids