proposition: Lemma zip_cat s1 s2 t1 t2 : size s1 = size t1 -> zip (s1 ++ s2) (t1 ++ t2) = zip s1 t1 ++ zip s2 t2.
proof: Proof. by move: s1 t1; apply: seq_ind2 => //= x y s1 t1 _ ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)