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. 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.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.NegativePropositions.