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