proposition: Lemma perm_zip_sym (S T : eqType) (s1 s2 : seq S) (t1 t2 : seq T) : perm_eq (zip s1 t1) (zip s2 t2) -> perm_eq (zip t1 s1) (zip t2 s2).
proof: Proof. have swap t s : zip t s = map (fun u => (u.2, u.1)) (zip s t). by elim: s t => [|x s +] [|y t]//= => ->. by rewrite [zip t1 s1]swap [zip t2 s2]swap; apply: perm_map. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)