Round-six lemma `ceil_bnd_le`