proposition: Lemma foldl_cat' T R f (z0 : R) (s1 s2 : seq T) : foldl f z0 (s1 ++ s2) = foldl f (foldl f z0 s1) s2.
proof: Proof. move: s1 z0. elim. done. move=> x xs IH. move=> acc. rewrite /=. by rewrite IH. Restart. Proof. by elim: s1 z0 => [//|x xs IH] acc /=; rewrite IH. Qed.
imports: mathcomp(all_ssreflect)