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