Round-six lemma `cY_le`