Round-six lemma `sp_rgP`