Round-six lemma `swapE_le`