Theorem associativityOfProducts_seq (M:monoid) : isAssociative_seq (unel M) (@op M). Proof. unfold isAssociative_seq; intros. induction x as [n x]. induction n as [|n IHn]. { reflexivity. } change (flatten _) with (flatten ((n,,x): NonemptySequence _)). rewrite flattenStep. change (lastValue _) with (x lastelement). unfold iterop_seq_seq. simpl. unfold iterop_fun_fun. rewrite (iterop_fun_step _ _ (lunax M)). generalize (x lastelement) as z; intro z. unfold iterop_seq. induction z as [m z]. induction m as [|m IHm]. { simpl. rewrite runax. simple refine (_ @ IHn (x ∘ dni lastelement)). rewrite concatenate'_r0. now apply (two_arg_paths_b (natplusr0 (stnsum (length ∘ (x ∘ dni lastelement))))). } change (length (S m,, z)) with (S m). change (sequenceToFunction (S m,,z)) with z. rewrite (iterop_fun_step _ _ (lunax M)). rewrite concatenateStep. generalize (z lastelement) as w; intros. rewrite <- assocax. unfold append. Opaque iterop_fun. simpl. Transparent iterop_fun. rewrite (iterop_fun_append _ _ (lunax M)). apply (maponpaths (λ u, u*w)). simpl in IHm. apply IHm. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Algebra.Groups. Require Import UniMath.MoreFoundations.NegativePropositions.