proposition: Lemma grinvandmonoidfun (X Y : gr) {f : X -> Y} (is : ismonoidfun f) (x : X) : paths (f (grinv X x)) (grinv Y (f x)).
proof: Proof. apply (grrcan Y (f x)). rewrite (pathsinv0 (pr1 is _ _)). rewrite (grlinvax X). rewrite (grlinvax Y). apply (pr2 is). Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids