Round-six lemma `isPiv_side`