Theorem commutativityOfProducts {M:abmonoid} {n} (x:stn n->M) (f:stn n ≃ stn n) : iterop_seq_mon (n,,x) = iterop_seq_mon (n,,x∘f). Proof. intros. induction n as [|n IH]. - reflexivity. - set (i := @lastelement n); set (i' := f i). rewrite (iterop_seq_mon_step (x ∘ f)). change ((x ∘ f) lastelement) with (x i'). rewrite (commutativityOfProducts_helper x i'). apply (maponpaths (λ k, k*_)). set (f' := weqoncompl_ne f i (stnneq i) (stnneq i') : stn_compl i ≃ stn_compl i'). set (g := weqdnicompl i); set (g' := weqdnicompl i'). apply pathsinv0. set (h := (invweq g' ∘ f' ∘ g)%weq). assert (L : x ∘ f ∘ dni lastelement ~ x ∘ dni i' ∘ h). { intro j. unfold funcomp. apply maponpaths. apply (invmaponpathsincl _ ( isinclstntonat _ ) _ _). unfold h. rewrite 2 weqcomp_to_funcomp_app. rewrite pr1_invweq. induction j as [j J]. unfold g, i, f', g', stntonat. rewrite <- (weqdnicompl_compute i'). unfold pr1compl_ne. rewrite homotweqinvweq. rewrite (weqoncompl_ne_compute f i (stnneq i) (stnneq i') _). apply maponpaths, maponpaths. apply subtypePath_prop. unfold stntonat. now rewrite weqdnicompl_compute. } rewrite (IH (x ∘ dni i') h). now apply iterop_seq_mon_homot. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.NegativePropositions.