proposition: Lemma map_sorted : forall (m: t elt)(Hm : sort (@ltk elt) m)(f:elt -> elt'), sort (@ltk elt') (map f m).
proof: Proof. induction m; simpl; auto. intros. destruct a as (x',e'). inversion_clear Hm. constructor; auto. exact (map_lelistA _ _ H0). Qed.
imports: FMapInterface