proposition: Lemma foldl_init (s : seq A) (x y : R) : foldl a (x \+ y) s = foldl a x s \+ y.
proof: Proof. by elim: s x y=>[|k s IH] x y //=; rewrite H IH. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)