Round-six lemma `GREC_split`