proposition: Lemma zip_fnd f1 f2 f x (v : V) : zip f1 f2 = Some f -> fnd x f = Some v -> exists v1, exists v2, [/\ zip_f v1 v2 = Some v, fnd x f1 = Some v1 & fnd x f2 = Some v2].
proof: Proof. case: f1 f2 f=>s1 H1 [s2 H2] [s3 H3] /=; move: (zip_sorted' _). case E1: (zip' s1 s2)=>[s|//] pf [E]; rewrite /fnd /=. clear H1 H2 H3 pf; rewrite -{s3}E. elim: s1 s2 s E1=>[|[k1 v1] s1 IH]; case=>[|[k2 v2] s2] //= s. - by case=><-. case: eqP=>// <-{k2}; case E1: (zip_f v1 v2)=>[w|//]. case E2: (zip' s1 s2)=>[t|//][<-{s}] /=. case: eqP=>[_ [<-]|_]; first by exists v1, v2. by case: (filter (predk V x) t) (IH _ _ E2). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)