proposition: 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: 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.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.PartA UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.NumberSystems.NaturalNumbersAlgebra