proposition: Theorem nat_plus_commutativity : isCommutative_fun_mon nataddabmonoid.
proof: Proof. intros ? ? ?. apply weqtoeqstn. intermediate_weq (∑ i, stn (x i)). - intermediate_weq (∑ i, stn (x(f i))). + apply invweq. rewrite iterop_fun_nat. apply weqstnsum1. + apply (weqfp _ (stn∘x)). - rewrite iterop_fun_nat. apply weqstnsum1. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Archimedean UniMath.Algebra.Domains_and_Fields UniMath.Algebra.IteratedBinaryOperations