proposition: 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: Proof. intros. refine (_ @ associativityOfProducts_seq M (partition f x)). assert (L := flatten_partition f x). apply pathsinv0. exact (iterop_seq_mon_homot _ _ L). Defined.
imports: UniMath.Combinatorics.Lists UniMath.Combinatorics.FiniteSequences UniMath.Algebra.RigsAndRings UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.Algebra.Groups UniMath.MoreFoundations.NegativePropositions