proposition: Lemma is_empty_spec m : is_empty m = true <-> forall x, find x m = None.
proof: Proof. destruct m as [|(k,e) m]; simpl; split; trivial; try discriminate. intros H. specialize (H k). now rewrite compare_refl in H. Qed.
imports: Coq(OrdersFacts OrdersLists)