proposition: Lemma add_neq_in_iff : forall m x y e, ~ E.eq x y -> (In y (add x e m) <-> In y m).
proof: Proof. split; intros (e',H0); exists e'. - apply (add_3 H H0). - apply add_2; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface