proposition: Lemma zip_rem f1 f2 f x : zip f1 f2 = Some f -> zip (rem x f1) (rem x f2) = Some (rem x f).
proof: Proof. case: f1 f2 f=>s1 H1 [s2 H2] [s3 H3] /=; do 2![move: (zip_sorted' _)]. case E1: (zip' s1 s2)=>[t|//]; case E2 : (zip' _ _)=>[q|]; rewrite (@zip_filter' _ _ _ _ E1) // in E2. by case: E2=><-{q} pf1 pf2 [E]; congr Some; apply/fmapE; rewrite /= E. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)