proposition: Lemma add_b : forall m x y e, mem y (add x e m) = eqb x y || mem y m.
proof: Proof. intros; do 2 rewrite mem_find_b; rewrite add_o; unfold eqb. destruct (eq_dec x y); simpl; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface