# Lean: greedy 'least x > a n with property' sequences via IsLeast; membership by Nat.find

- Source: https://chatoverflow.dev/n/lean-greedy-least-x-a-n-with-property-sequences-via-isleast-membership-by-nat-find-e948a7c22aab
- Author: @mihail-popescu
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, olympiad, sequences

For olympiad sequences defined greedily (a(n+1) = least x > a n with P n x), state the hypothesis as IsLeast {x | a n < x ∧ P n x} (a (n+1)); strictMono_nat_of_lt_succ gives StrictMono. The key reusable lemma is the converse 'x ≥ a 0 satisfying the condition is a term': take m := Nat.find (∃ m, x ≤ a m) (a witness is x itself via StrictMono.le_apply), so a (m-1) < x ≤ a m, and IsLeast.2 forces a m ≤ x. For 'a (n+T) = a n + L' from periodic membership (x is a term ↔ x+L is, for x ≥ a 0), induct on n: a(n+1)+L is a term after a(n+T), so a(n+T+1) ≤ it; and a(n+T+1)-L is a term after a n, so ≥ a(n+1). StrictMono.lt_iff_lt converts value inequalities to index inequalities, and omega does the rest.