proposition: Lemma zip_supp f1 f2 f : zip f1 f2 = Some f -> supp f =i supp f1.
proof: Proof. case: f1 f2 f=>s1 H1 [s2 H2] [s3 H3] /=; move: (zip_sorted' _). case E: (zip' s1 s2)=>[t|//]; move=>pf [F x]; rewrite -{s3}F in H3 *. by rewrite /supp (zip_supp' E). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)