proposition: Lemma fnd_kfilt (p : pred K) k (s : fmap) : fnd k (kfilter p s) = if p k then fnd k s else None.
proof: Proof. case: s; rewrite /fnd /kfilter /kfilter' /=. elim=>[|[k1 v] s IH] /=; first by case: ifP. move/path_sorted=>{}/IH H. case: ifP=>E1 /=; first by case: ifP=>E2 //; rewrite -(eqP E2) E1. case: ifP H=>E2 H //=; rewrite H; case: eqP=>// E3. by rewrite -E3 E1 in E2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)