feat: filter MePo candidates to theorems and order output by iteration

This PR refines MePo premise selection so that (1) candidates are restricted
to theorems, matching the convention already used by `SineQuaNon` and
`SymbolFrequency`, and (2) the result is ordered lexicographically by
`(iteration, score)` rather than by score alone.

Before the theorem filter, `mepoSelector` returned functions, recursors, and
casts (e.g. `Int.add`, `Eq.ndrec`, `cast`, `proof_irrel`) alongside real
premises. With it, those go away and the obvious lemmas — e.g. `Int.add_comm`
for `a + b = b + a` — rank well above the remaining noise.

The `(iteration, score)` ordering preserves the iteration priority of the
original Meng–Paulson MePo: an iter-1 premise scoring 0.6 always ranks above
an iter-2 premise scoring 1.0, since later iterations score against a strictly
larger `relevant` set and a higher threshold, so their raw scores are not
comparable.

Thanks to Xavier Généreux for the report. Further tuning of the score function
is tracked in https://github.com/leanprover/lean4/issues/13749.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>