Theorem nat_plus_commutativity : isCommutative_fun_mon nataddabmonoid. 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.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.NegativePropositions.