Corollary associativityOfProducts' {M:monoid} {n} (f:stn n → nat) (x:stn (stnsum f) → M) : iterop_seq_mon (stnsum f,,x) = iterop_seq_seq_mon (partition f x). Proof. intros. refine (_ @ associativityOfProducts_seq M (partition f x)). assert (L := flatten_partition f x). apply pathsinv0. exact (iterop_seq_mon_homot _ _ L). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.NegativePropositions.