Round-six lemma `atanP_spec`