proposition: Lemma add_spec2' m x y e : ~X.eq x y -> find y (add x e m) = find y m.
proof: Proof. induction m as [|(k,e') m IH]; simpl. - case X.compare_spec; trivial; MX.order. - case X.compare_spec; simpl; intros; trivial. + rewrite <-H. case X.compare_spec; trivial; MX.order. + do 2 (case X.compare_spec; trivial; try MX.order). + now rewrite IH. Qed.
imports: Coq(OrdersFacts OrdersLists)