Round-six lemma `depH_le_log`