proposition: Lemma grinvunel (X : gr) : paths (grinv X (unel X)) (unel X).
proof: Proof. apply (grrcan X (unel X)). rewrite (grlinvax X). rewrite (runax X). apply idpath. Defined.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids