Round-six lemma `leB_sound`