Lemma commutativityOfProducts_helper {M:abmonoid} {n} (x:stn (S n) → M) (j:stn (S n)) : iterop_seq_mon (S n,,x) = iterop_seq_mon (n,,x ∘ dni j) * x j. Proof. induction j as [j jlt]. assert (jle := natlthsntoleh _ _ jlt). Local Open Scope transport. set (f := nil □ j □ S O □ n-j : stn 3 → nat). assert (B : stnsum f = S n). { unfold stnsum, f; simpl. repeat unfold append_vec; simpl. rewrite natplusassoc. rewrite (natpluscomm 1). rewrite <- natplusassoc. rewrite natpluscomm. apply (maponpaths S). rewrite natpluscomm. now apply minusplusnmm. } set (r := weqfibtototal _ _ (λ k, eqweqmap (maponpaths (λ n, k < n : UU) B) ) : stn (stnsum f) ≃ stn (S n)). set (x' := x ∘ r). intermediate_path (iterop_seq_mon (stnsum f,, x')). { induction B. apply iterop_seq_mon_homot. intros i. unfold x'. simpl. apply maponpaths. apply ( invmaponpathsincl _ ( isinclstntonat _ ) _ _). reflexivity. } unfold iterop_seq_mon. unfold iterop_seq. refine (associativityOfProducts' f x' @ _). unfold partition. rewrite 3 iterop_seq_seq_mon_step. change (iterop_seq_seq_mon (0,,_)) with (unel M); rewrite lunax. set (s0 := dni lastelement (dni lastelement (@lastelement 0))). unfold funcomp at 1 2 3. set (s1 := dni lastelement (@lastelement 1)). set (s2 := @lastelement 2). unfold partition'. unfold inverse_lexicalEnumeration. change (f s0) with j; change (f s1) with (S O); change (f s2) with (n-j). set (f' := nil □ j □ n-j : stn 2 → nat). assert (B' : stnsum f' = n). { unfold stnsum, f'; simpl. repeat unfold append_vec; simpl. rewrite natpluscomm. now apply minusplusnmm. } set (r' := weqfibtototal _ _ (λ k, eqweqmap (maponpaths (λ n, k < n : UU) B') ) : stn (stnsum f') ≃ stn n). set (x'' := x ∘ dni (j,, jlt) ∘ r'). intermediate_path (iterop_seq_mon (stnsum f',, x'') * x (j,, jlt)). { assert (L := iterop_seq_mon_len1 (λ j0 : stn 1, x' ((weqstnsum1 f) (s1,, j0)))). unfold functionToSequence in L. rewrite L. rewrite assocax. refine (transportf (λ k, _*k=_) (commax _ _ _) _). rewrite <- assocax. apply two_arg_paths. { refine (_ @ !associativityOfProducts' f' x''). unfold partition. rewrite 2 iterop_seq_seq_mon_step. change (iterop_seq_seq_mon (0,,_)) with (unel M); rewrite lunax. apply two_arg_paths. { unfold funcomp. set (s0' := dni lastelement (@lastelement 0)). unfold partition'. change (f' s0') with j. apply iterop_seq_mon_homot. intro i. unfold x', x'', funcomp. apply maponpaths. apply subtypePath_prop. change_lhs (stntonat _ i). unfold dni. unfold di. unfold stntonat. match goal with |- context [ match ?x with _ => _ end ] => induction x as [c|c] end. { reflexivity. } { apply fromempty. assert (P := c : i ≥ j); clear c. exact (natlthtonegnatgeh _ _ (stnlt i) P). } } { unfold partition'. change (f' lastelement) with (n-j). apply iterop_seq_mon_homot. intro i. unfold x', x'', funcomp. apply maponpaths. apply subtypePath_prop. change_lhs (j+1+i). unfold dni, di. unfold stntonat. match goal with |- context [ match ?x with _ => _ end ] => induction x as [c|c] end. { apply fromempty. exact (negnatlthplusnmn j i c). } { change_rhs (1 + (j + i)). rewrite <- natplusassoc. rewrite (natpluscomm j 1). reflexivity. } } } unfold x'; simpl. apply maponpaths. apply subtypePath_prop. change (j+0 = j). apply natplusr0. } { apply (maponpaths (λ k, k * _)). induction (!B'). change_rhs (iterop_seq_mon (n,, x ∘ dni (j,, jlt))). apply iterop_seq_mon_homot; intros i. unfold x''; simpl. apply maponpaths. apply ( invmaponpathsincl _ ( isinclstntonat _ ) _ _). reflexivity. } Qed.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.NegativePropositions.