Round-six lemma `eval_le_mg`