Theorem associativityOfProducts_list (M:monoid) : isAssociative_list (unel M) (@op M). Proof. unfold isAssociative_list. apply list_ind. - simpl. reflexivity. - intros x xs I. simpl in I. rewrite Lists.flattenStep. refine (iterop_list_mon_concatenate _ _ @ _). unfold iterop_list_list. rewrite mapStep. rewrite (iterop_list_step _ _ (runax M)). + apply (maponpaths (λ x, _ * x)). exact I. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.NegativePropositions.