Round-six lemma `psw_mul`