proposition: Lemma foldl_helper (s1 s2 : seq A) (z0 : R) x : foldl a z0 (s1 ++ x :: s2) = foldl a z0 (x :: s1 ++ s2).
proof: Proof. elim: s1 s2 z0=>[|k ks IH] s2' z0 //=. rewrite IH /=; congr foldl. rewrite -[a z0 k]unitL H -[z0]unitL !H. by rewrite -{2}[a Unit x]unitL H joinCA joinA. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)