Lemma nat_to_monoid_unel' {X : abgr} (x : X) (n : nat) : ((nat_to_monoid_fun x n) * (nat_to_monoid_fun (grinv X x) n))%multmonoid = (unel X). Proof. induction n as [ | n IHn]. - use (runax X). - Opaque nat_to_monoid_fun. cbn in *. rewrite (@nat_to_monoid_fun_S X x). rewrite (@nat_to_monoid_fun_S X (grinv X x)). rewrite (commax X _ x). rewrite (assocax X). rewrite <- (assocax X (@nat_to_monoid_fun X x n)). use (pathscomp0 (maponpaths (λ xx : pr1 X, (x * (xx * (grinv X x))))%multmonoid IHn)). clear IHn. use (pathscomp0 _ (grrinvax X x)). use two_arg_paths. + use idpath. + use (lunax X). Qed.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.