proposition: Lemma zipwithE s1 s2 : zipwith s1 s2 = [seq f x.1 x.2 | x <- zip s1 s2].
proof: Proof. by elim: s1 s2 => [|x1 s1 ihs1] [|x2 s2] //=; rewrite ihs1. Qed.
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)