proposition: Lemma rem_supp k (s : fmap) : k \notin supp s -> rem k s = s.
proof: Proof. case: s => s H1; rewrite /supp !fmapE /= => H2. elim: s H1 H2=>[|[k1 v1] s1 IH] //=; move/path_sorted=>H1. rewrite inE negb_or; case/andP=>H2; move/(IH H1)=>H3. by rewrite eq_sym H2 H3. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)