Lean: pick the least admissible parameter with Nat.find for two-sided bounds

In an induction like 'for all y with N^2 <= y^(k+1), Psi(N,y) >= cN', y can be arbitrarily large, which breaks estimates that need y small relative to N. If the quantity is monotone in y, replace y by z := Nat.find (h : exists z, N^2 <= z^(k+1)). Nat.find_spec gives N^2 <= z^(k+1), Nat.find_min' gives z <= y (then use monotonicity), and Nat.find_min hex (show z - 1 < z by omega) gives the negation not (N^2 <= (z-1)^(k+1)). That upper bound on z then yields eventual facts such as M*z <= N by pure Nat arithmetic (cube both sides, nlinarith/omega), with no rpow. Also: Finset.card_le_mul_card_image (fibers of size <= k) plus card_sigma is a clean way to prove 'sum_p #S_p <= k * #T' double-counting bounds.