proposition: Lemma mem_2 : forall m x, mem x m = true -> In x m.
proof: Proof. unfold In, MapsTo; intros m x; rewrite mem_find. destruct (find x m). - exists a; auto. - intros; discriminate. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface