proposition: Lemma foldl_perm (s1 s2 : seq A) (z0 : R) : perm s1 s2 -> foldl a z0 s1 = foldl a z0 s2.
proof: Proof. move=>P; elim: s1 s2 z0 P=>[|k ks IH] s2 z0 P; first by move/pperm_nil: P=>->. have K: k \In s2 by apply: pperm_in P _; rewrite InE; left. case: {K} (In_split K) P=>x [y] ->{s2} /= /pperm_cons_cat_cons P. by rewrite foldl_helper //=; apply: IH. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)