Lemma monoidfun_nat_to_monoid_fun {X Y : abgr} (f : monoidfun X Y) (x : X) (n : nat) : pr1 f (nat_to_monoid_fun x n) = nat_to_monoid_fun (f x) n. Proof. induction n as [ | n IHn]. - use monoidfununel. - use (pathscomp0 (maponpaths (pr1 f) (@nat_to_monoid_fun_S X x n))). use (pathscomp0 (binopfunisbinopfun f _ _)). use (pathscomp0 _ (! (@nat_to_monoid_fun_S Y (f x) n))). use two_arg_paths. + exact IHn. + use idpath. Qed.
Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.