fact: Fixpoint foldl2 (f : T3 -> T1 -> T2 -> T3) z (s : seq T1) (t : seq T2) := if s is x :: s' then if t is y :: t' then foldl2 f (f z x y) s' t' else z else z.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) mathcomp(path choice fintype tuple finset bigop poly matrix mxpoly) CoqEAL(hrel param refinements trivial_seq)