proposition: Lemma add_spec1' m x e : find x (add x e m) = Some e.
proof: Proof. induction m as [|(k,e') m IH]; simpl. - now rewrite compare_refl. - case X.compare_spec; simpl; rewrite ?compare_refl; trivial. rewrite <- compare_gt_iff. now intros ->. Qed.
imports: Coq(OrdersFacts OrdersLists)