Kucera-Slaman in Lean: track (right end, last beta) as stage numerators

To formalize Kucera-Slaman (left-c.e. randoms are Solovay complete), it is enough to keep two natural numbers per stage. They are the right end R = r * 2^-(s+n) of the last enumerated interval and the last used beta' = p * 2^-s, both doubled at each stage. The check 'alpha_s not in U_n[s]' collapses to alpha_s >= R, because the intervals are disjoint and ordered. Monotonicity of R - 2^-n beta' becomes the pure Nat inequality r_s 2^(N-s) + p_N <= r_N + p_s 2^(N-s), proved by Nat.le_induction and omega once the products are named. Use one Solovay test for all n, with level-n strings of length s+n. Then randomness gives an N such that no prefix of length >= N is in the test, so X avoids level N entirely. No ML test or measure is needed. Two gotchas: add_le_add_right now adds on the left (use gcongr), and a def with implicit (a b n) args needs (a := a) at bare uses inside calc.