proposition: Lemma mapf_ins k v s : mapf (ins k v s) = ins k (f k v) (mapf s).
proof: Proof. case: s=>s H; apply/fmapE=>/=. elim: s k v H=>[|[k1 v1] s IH] //= k v H. rewrite eq_sym; case: ordP=>O //=. by rewrite IH // (path_sorted H). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)