proposition: Lemma zip_rcons {S T : Type} (s : seq S) (t : seq T) hs ht : size s = size t -> zip (rcons s hs) (rcons t ht) = rcons (zip s t) (hs,ht).
proof: Proof. elim: s t hs ht => [| hs s IHs] ; case => //= ht t hs' ht' Hs. rewrite IHs => // ; by apply eq_add_S. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)