proposition: Lemma remove_sorted : forall m (Hm:Sort m) x, Sort (remove x m).
proof: Proof. induction m. - simpl; intuition. - intros. destruct a as (x',e'). simpl; case (X.compare x x'); intuition; inversion_clear Hm; auto. Qed.
imports: FMapInterface