proposition: Lemma remove_spec1 m x {Hm:Ok m} : find x (remove x m) = None.
proof: Proof. induction m as [|(k,e') m IH]; simpl; trivial. inversion_clear Hm; chok. case X.compare_spec; simpl. - intros E. rewrite <- E in H0. apply Sort_Inf_NotIn in H0; trivial. assert (F := @find_spec m x). destruct (find x m); trivial. elim H0; exists e. rewrite <- (F e); auto. - rewrite <- compare_lt_iff. now intros ->. - rewrite <- compare_gt_iff. intros ->; auto. Qed.
imports: Coq(OrdersFacts OrdersLists)