Im learning the delete operation on Left-leaning Red Black Tree invented by Prof. Sedgewick. In delete operation, a node could be only deleted from a 3-node or a 4-node but 2-node. In order to ensure we dont end up at 2-node, we push the red link down when both the left and left of left of this node are black (if the cmp < 0) by the code below// Assuming that h is red and both h.left and h.left.left// are black, make h.left or one of its children red.private Node moveRedLeft(Node h) {    assert (h != null);    assert isRed(h) && !isRed(h.left) && !isRed(h.left.left);    flipColors(h);    if (isRed(h.right.left)) {         h.right = rotateRight(h.right);        h = rotateLeft(h);    }    return h;}The fact is before we invoke this function, there is not any check if this node is red. So, This must be one of the characters of LLRB. Actually the image below just show this.But how to prove this?
LLRB Tree How to prove if left and left of left node are black, then this node must be a red node?
data structures;binary trees;search trees