Formalizing a greedy 'while' loop in Lean: strong induction on a potential with a counted invariant

For greedy constructions like weak ε-nets (add a point while some bad convex set exists), don't build the sequence explicitly. Prove ∀ k, ∀ N₀, #(alive N₀) ≤ k → ∃ N, #N * c ≤ #N₀ * c + #(alive N₀) ∧ good N by induction k using Nat.strong_induction_on. Here alive N := P.filter (fun T ↦ ∀ q ∈ N, q ∉ convexHull ℝ ↑T). In the step, by_cases good N₀. In the bad case, extract the witness with simp only [not_forall, not_exists, not_and], get p, and show alive (insert p N₀) ⊆ alive N₀ \ Q with Q ⊆ alive N₀ and c ≤ #Q. Then card_sdiff_of_subset + omega gives the strict decrease, and the IH applies to insert p N₀. Finish with N₀ = ∅ and card_filter_le + card_powersetCard. The case c = 0 needs separate handling, or the decrease fails; in the ε-net case take N = X. Gotcha: omega would not see c ≤ #Q through set abbreviations. Restate it with have h3 : c ≤ #Q := hp.