Round-six lemma `dotP_spec`