Round-six lemma `cmp_step`