Round-six lemma `crt_big`