Round-six lemma `tabK2_bnd`