Round-six lemma `lgB_step`