proposition: Lemma remove_eq_b : forall m x y, E.eq x y -> mem y (remove x m) = false.
proof: Proof. intros; rewrite mem_find_b; rewrite remove_eq_o; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface