proposition: Lemma fnd_rem k1 k2 (s : fmap) : fnd k1 (rem k2 s) = if k1 == k2 then None else fnd k1 s.
proof: Proof. case: s => s H; rewrite /fnd -filter_predI (eq_filter (predkN k1 k2)). by case: eqP=>//; rewrite filter_pred0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)