Proof of an $\iff$ statement on binary trees 
Let $x$ and $y$ be two nodes of a binary tree $B$.
Prove that $x$ is an ancestor of $y$ $\iff$ $x$ stands before $y$ in the pre-order traversal of $B$ and $x$ stands  after $y$ in the post-order traversal of $B$.

I can do the $\implies$ part without trouble, but I can't deal with the converse with enough rigour.
Thanks for any kind of rigorous proof.
 A: For the converse I would proceed by contrapositive with the following ideas.
(1) Assume $x$ and $y$ are vertices for which neither is an ancestor of the other.
(2) Argue that there is a lowest common ancestor (I am picturing the tree drawn with the root at the top and going downwards) of $x$ and $y$, say $a$.
(3) Argue that one of $x$ and $y$, say $x$ is a left descendant of $a$ and the other is a right descendant of $a$.  (If both are on the same side of $a$, then there is a lower common ancestor.)
(4) Then in preorder traversal, these three vertices will be in order $a$...$x$...$y$, and in postorder traversal $x$...$y$...$a$.  
A: $\Longleftarrow$: Assume that (a) $x$ stands before $y$ in the pre-order traversal of $B$ and that (b) $x$ stands after $y$ in the post-order traversal of $B$.
Now assume that (c) $x$ is not an ancestor of $y$ (a proof by contradiction will follow). There are two cases:


*

*$y$ is an ancestor of $x$: a node $u$ isn't visited by pre-order traversal until all of its ancestors have been visited. So if $y$ is an ancestor of $x$, then $y$ will be visited before $x$ in pre-order traversal. This contradicts (a).

*(d) $y$ is not an ancestor of $x$: neither $x$ nor $y$ is the root, for otherwise one would be the ancestor of the other (contradicting either (c) or (d)). Thus there definitely exists at least one common ancestor. Let the lowest common ancestor $a$ be the first ancestor that you encounter when you trace the paths upward from $x$ and $y$ towards the root. There are three cases:


*

*Both $x$ and $y$ are in the same subtree $T$ of $a$: since $a$ is the lowest common ancestor, either $x$ or $y$ is the root $r$ of $T$ (otherwise, $r$ would be the lowest common ancestor of $x$ and $y$, contradicting the fact that $a$ is). Thus either $x$ is an ancestor of $y$ or $y$ is an ancestor of $x$. This contradicts either (c) or (d).

*$x$ is in the left subtree of $a$, and $y$ is in the right subtree of $a$: in post-order traversal, a left subtree of some root $r$ will be visited exhaustively before any node in the right subtree of $r$ will be visited (cite pseudocode if you desire more rigour). Thus $x$ will be visited before $y$ in post-order traversal. This contradicts (b).

*$x$ is in the right subtree of $a$, and $y$ is in the left subtree of $a$: in pre-order traversal, a left subtree of some root $r$ will be visited exhaustively before any node in the right subtree of $r$ will be visited (cite pseudocode if you desire more rigour). Thus $y$ will be visited before $x$ in pre-order traversal. This contradicts (a).



Since (c) results in only contradictions under the assumption of (a) and (b), its negation, i.e. that $x$ is an ancestor of $y$, must follow from the conjunction of (a) and (b).
Is this sufficiently rigorous?
A: The result is true for any rooted tree (assuming that the children of each node are visited in the same order regardless of the type of traversal).
The key fact is that $x$ is an ancestor of $y$ iff $x = \operatorname{lca}(x,y)$ (where $\operatorname{lca}(x,y)$ denotes the lowest common ancestor of $x,y$).
Now suppose $x$ is an ancestor of $y$. Then in the pre-order traversal, $x$ must precede $y$, and in the post-order traversal $y$ must precede $x$.
Now suppose $x$ is not an ancestor of $y$. Let $l=\operatorname{lca}(x,y)$, and we know that $x \neq l$. Let $S(v)$ represent the nodes in the subtree rooted at $v$ (including $v$), and let $c_1,...c_k$ be the children of $l$.
We have $x \in S(c_{i_1})$, $y \in S(c_{i_2})$ for some indices $i_1, i_2$.
Suppose $i_1 < i_2$, then in the pre-order traversal $l$ will precede $x$ and $x$ will precede $y$, and in the post-order traversal $x $ will precede $y$ and $y$ will precede $l$. Similarly if $i_1>i_2$ with the roles of $x,y$ interchanged.
