proposition: Lemma iterop_list_mon_concatenate {M : monoid} (l s : list M) : iterop_list_mon (Lists.concatenate l s) = iterop_list_mon l * iterop_list_mon s.
proof: Proof. revert l. apply list_ind. - apply pathsinv0, lunax. - intros x xs J. rewrite Lists.concatenateStep. unfold iterop_list_mon. rewrite 2 (iterop_list_step _ _ (runax M)). rewrite assocax. apply maponpaths. exact J. Defined.
imports: UniMath.Combinatorics.Lists UniMath.Combinatorics.FiniteSequences UniMath.Algebra.RigsAndRings UniMath.Foundations.UnivalenceAxiom UniMath.MoreFoundations.Tactics UniMath.Algebra.Groups UniMath.MoreFoundations.NegativePropositions