proposition: Lemma supp_rem k (s : fmap) : supp (rem k s) =i predI (predC1 k) (mem (supp s)).
proof: Proof. case: s => s H1 x; rewrite /supp inE /=. by case H2: (x == k)=>/=; rewrite -filter_map mem_filter /= H2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)