proposition: Lemma zip_nil_2 : forall (s : seq R), zip s (@nil R) = [::].
proof: Proof. by case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path choice fintype order) mathcomp(prime div bigop ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex)