Round-six lemma `cTot_le`