Round-six lemma `CNs2_lt`