proposition: Lemma add_neq_b : forall m x y e, ~E.eq x y -> mem y (add x e m) = mem y m.
proof: Proof. intros; do 2 rewrite mem_find_b; rewrite add_neq_o; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface