proposition: Lemma zip_rcons s t x y : size s = size t -> zip (rcons s x) (rcons t y) = rcons (zip s t) (x, y).
proof: Proof. by move=> eq_sz; rewrite -!cats1 zip_cat //= eq_sz. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)