proposition: Lemma eq_seqE (T : Type) (f : T -> T -> bool) s1 s2 : size s1 = size s2 -> eq_seq f s1 s2 = all (fun xy => f xy.1 xy.2) (zip s1 s2).
proof: Proof. elim: s1 s2 => [|x1 s1 IHs] [] //= x2 s2 /eqP eq_sz. by rewrite IHs //; apply/eqP. 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)