Height_Balanced_Tree_Bounds.HBT_Lemma_Bucket