proposition: Lemma grinvinv (X : gr) (a : X) : paths (grinv X (grinv X a)) a.
proof: Proof. apply (grlcan X (grinv X a)). rewrite (grlinvax X a). rewrite (grrinvax X _). apply idpath. Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids