proposition: Lemma sorted_map (m : seq (K * U)) : sorted ord (map key m) -> sorted ord (map key (mapf' m)).
proof: Proof. elim: m=>[|[k v] m IH] //= H. rewrite path_min_sorted; first by apply: IH; apply: path_sorted H. rewrite map_key_mapf. by apply/(order_path_min _ H);apply/trans. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path) pcm(options)