prove correctness of in-order tree traversal subroutine
In your proof the largest element of binary search tree $T$ can in fact be the root of the tree. I did not check whether you took care of that.
If you want to use induction by a number of elements in the tree, I would advise you to take strong induction, that is the hypothesis assumes the algorithm works for any number less or equal to $n$. Then the hypothesis can be applied to both subtrees which must have less elements than the full tree.
Finaly you could use structural induction, that is induction using the inductive definition of the structures you consider. Here that is the notion of a binary tree: which is either empty, or a root and two subtrees. In practise this gives the same proof as strong induction, but you did not need to quantify the number of nodes.