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

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.