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