proposition: Lemma add_find : forall m x y e, bst m -> find y (add x e m) = match X.compare y x with EQ _ => Some e | _ => find y m end.
proof: Proof. intros. assert (~X.eq x y -> find y (add x e m) = find y m). - intros; rewrite find_mapsto_equiv; auto. split; eauto using add_2, add_3. - destruct X.compare; try (apply H0; order). auto using find_1, add_1 with ordered_type. Qed.
imports: FunInd FMapInterface FMapList ZArith Int