proposition: Lemma supp_kfilt (p : pred K) (s : fmap) : supp (kfilter p s) = filter p (supp s).
proof: Proof. case: s; rewrite /supp /kfilter /kfilter' /=. elim=>[|[k v] s IH] //= /path_sorted {}/IH H. by case E: (p k)=>//=; rewrite H. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)