Proved lemma 13.1, and use it to prove claim of red-black BST running-time.