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.

$\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?
