proposition: Lemma rev_zip s t : size s = size t -> rev (zip s t) = zip (rev s) (rev t).
proof: Proof. move: s t; apply: seq_ind2 => //= x y s t eq_sz IHs. by rewrite !rev_cons IHs zip_rcons ?size_rev. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)