tree* tree_insert(tree* T, elem e)
//@requires is_ordtree(T);
//@requires e != NULL;
//@ensures is_ordtree(\result);
{
    if (T == NULL) {
        /* create new node and return it */
        T = alloc(struct tree_node);
        T->data = e;
        T->left = NULL;
        T->right = NULL;
        return T;
    }
    int r = key_compare(elem_key(e), elem_key(T->data));
    if (r == 0) {
        T->data = e;		/* modify in place */
    }
    else if (r < 0) {
        T->left = tree_insert(T->left, e);
    }
    else {
        //@assert r > 0;
        T->right = tree_insert(T->right, e);
    }
    return T;
}