proposition: Lemma notin_filter (x : K) s : x \notin (map key s) -> filter (predk V x) s = [::].
proof: Proof. elim: s=>[|[k v] s IH] //=. rewrite inE negb_or; case/andP=>H1 H2. by rewrite eq_sym (negbTE H1); apply: IH. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)