proposition: Lemma add_Inf : forall (m:t elt)(x x':key)(e e':elt), Inf (x',e') m -> ltk (x',e') (x,e) -> Inf (x',e') (add x e m).
proof: Proof. induction m. simpl; intuition. intros. destruct a as (x'',e''). inversion_clear H. compute in H0,H1. simpl; case X.compare; intuition. Qed.
imports: Coq(OrdersFacts OrdersLists)