proposition: Lemma add_neq_o : forall m x y e, ~ E.eq x y -> find y (add x e m) = find y m.
proof: Proof. intros. rewrite eq_option_alt. intro e'. rewrite <- 2 find_mapsto_iff. apply add_neq_mapsto_iff; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface