proposition: Lemma add_bst : forall m x e, bst m -> bst (add x e m).
proof: Proof. intros m x e; functional induction (add x e m); intros; inv bst; try apply bal_bst; auto; intro z; rewrite add_in; intuition. - apply MX.eq_lt with x; auto. - apply MX.lt_eq with x; auto with ordered_type. Qed.
imports: FunInd FMapInterface FMapList ZArith Int