proposition: Lemma rem_rem k1 k2 (s : fmap) : rem k1 (rem k2 s) = if k1 == k2 then rem k1 s else rem k2 (rem k1 s).
proof: Proof. rewrite /rem; case: s => s H /=. case H1: (k1 == k2); rewrite fmapE /= -!filter_predI; apply: eq_filter=>x /=. - by rewrite (eqP H1) andbb. by rewrite andbC. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)