Round-six lemma `fmB_le_log`