diff --git a/src/Lean/LibrarySuggestions/MePo.lean b/src/Lean/LibrarySuggestions/MePo.lean
index b719f59c59..27c499c29f 100644
--- a/src/Lean/LibrarySuggestions/MePo.lean
+++ b/src/Lean/LibrarySuggestions/MePo.lean
@@ -57,11 +57,16 @@ def mepo (initialRelevant : NameSet) (score : NameSet → NameSet → Float) (ac
       |>.partition fun (_, _, s) => p ≤ s
     if newAccepted.isEmpty then return accepted
     trace[mepo] m!"Accepted {newAccepted.map fun (n, _, s) => (n, s)}."
+    -- Scores from different iterations are not comparable: each iteration accepts
+    -- against a strictly larger `relevant` set and a higher threshold. We order the
+    -- output by `(iteration, score)`: earlier iterations always rank first, and
+    -- within an iteration we sort by descending score.
+    let newAccepted := newAccepted.qsort (fun (_, _, s₁) (_, _, s₂) => s₁ > s₂)
     accepted := newAccepted.foldl (fun acc (n, _, s) => acc.push { name := n, score := s }) accepted
     candidates := candidates'.map fun (n, c, _) => (n, c)
     relevant := newAccepted.foldl (fun acc (_, ns, _) => acc ++ ns) relevant
     p := p + (1 - p) / c
-  return accepted.qsort (fun a b => a.score > b.score)
+  return accepted
 
 end MePo
 
@@ -76,7 +81,8 @@ public def mepoSelector (useRarity : Bool) (p : Float := 0.6) (c : Float := 2.4)
     pure <| frequencyScore (fun n => frequency.getD n 0)
   else
     pure <| unweightedScore
-  let accept := fun ci => return !isDeniedPremise env ci.name
+  let accept := fun ci =>
+    return !isDeniedPremise env ci.name && wasOriginallyTheorem env ci.name
   let suggestions ← mepo constants score accept config.maxSuggestions p c
-  -- `mepo` already returns suggestions in score-descending order.
+  -- `mepo` already returns suggestions ordered by `(iteration, score)`.
   return suggestions.take config.maxSuggestions
diff --git a/tests/elab/library_suggestions_mepo_order.lean b/tests/elab/library_suggestions_mepo_order.lean
index 2e9b988e43..e83c1a0ef0 100644
--- a/tests/elab/library_suggestions_mepo_order.lean
+++ b/tests/elab/library_suggestions_mepo_order.lean
@@ -1,12 +1,13 @@
 import Lean.LibrarySuggestions.MePo
 
 /-!
-Regression test: the MePo premise selector must return suggestions in
-score-descending order.
+Regression test: the MePo premise selector filters candidates to theorems
+(matching the convention already used by `SineQuaNon` and `SymbolFrequency`)
+and finds the obvious lemma for an arithmetic equality goal.
 
-A stale `.reverse` in `mepoSelector` (left over from before the selector was
-made score-sorting) flipped the order to score-ascending, so `.take` returned
-the lowest-scoring premises instead of the best ones.
+Output is ordered by `(iteration, score)` rather than by score alone, so the
+score sequence is not globally monotonic — a score jump signals an iteration
+boundary.
 -/
 
 open Lean Lean.Elab.Tactic Lean.LibrarySuggestions
@@ -15,11 +16,13 @@ example (a b : Int) : a + b = b + a := by
   run_tac do
     let sel : Selector := mepoSelector (useRarity := false)
     let s ← sel (← getMainGoal) {}
-    let mut prev? : Option Float := none
-    for x in s do
-      if let some prev := prev? then
-        unless prev ≥ x.score do
-          throwError "MePo suggestions are not score-descending: \
-            score {prev} precedes score {x.score}"
-      prev? := some x.score
+    let names := s.map (·.name)
+    if names.contains ``Eq.ndrec then
+      throwError "Eq.ndrec (a recursor) should be filtered out by the theorem-only \
+        accept filter"
+    if names.contains ``Int.add then
+      throwError "Int.add (a function) should be filtered out by the theorem-only \
+        accept filter"
+    unless names.contains ``Int.add_comm do
+      throwError "Int.add_comm should appear in the MePo suggestions for `a + b = b + a`"
   sorry
diff --git a/tests/elab/library_suggestions_mepo_order.lean.out.expected b/tests/elab/library_suggestions_mepo_order.lean.out.expected
index bbb4d1c5fb..aa752520f4 100644
--- a/tests/elab/library_suggestions_mepo_order.lean.out.expected
+++ b/tests/elab/library_suggestions_mepo_order.lean.out.expected
@@ -1 +1 @@
-library_suggestions_mepo_order.lean:14:0-14:7: warning: declaration uses `sorry`
+library_suggestions_mepo_order.lean:15:0-15:7: warning: declaration uses `sorry`