proposition: Lemma kfilt_ins (p : pred K) k v (s : fmap) : kfilter p (ins k v s) = if p k then ins k v (kfilter p s) else kfilter p s.
proof: Proof. apply/fmapP=>k2; case: ifP=>E1. - by rewrite fnd_ins !fnd_kfilt fnd_ins; case: eqP=>// ->; rewrite E1. by rewrite !fnd_kfilt fnd_ins; case: eqP=>// ->; rewrite E1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)