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