Added valid_sub_bplustree_impl_valid_bplustree lemma