proposition: Lemma grinvop (Y : gr) : ∏ y1 y2 : Y, grinv Y (@op Y y1 y2) = @op Y (grinv Y y2) (grinv Y y1).
proof: Proof. intros y1 y2. apply (grrcan Y y1). rewrite (assocax Y). rewrite (grlinvax Y). rewrite (runax Y). apply (grrcan Y y2). rewrite (grlinvax Y). rewrite (assocax Y). rewrite (grlinvax Y). apply idpath. Qed.
imports: UniMath.MoreFoundations.Orders UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.Algebra.Monoids