Lemma nat_nat_to_monoid_plus1 {X : abgr} (x : X) {n1 m1 m2: nat} (e : m2 = (m1 + n1)%nat) : nat_to_monoid_fun (grinv X x) n1 = (nat_to_monoid_fun x m1 * nat_to_monoid_fun (grinv X x) m2)%multmonoid. Proof. rewrite e. clear e. rewrite nat_to_abmonoid_fun_plus. rewrite <- (assocax X). use pathsinv0. use (pathscomp0 (maponpaths (λ xx : X, (xx * (nat_to_monoid_fun (grinv X x) n1))%multmonoid) (nat_to_monoid_unel' x m1))). use (lunax X). Qed.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.