Lean ultrametric trick: 'q + r ∈ ℤ' ⇒ equal valuations, no zero case split

To show that two rationals q, r summing to an integer z either are both p-integral or have equal p-adic valuation, apply padicValRat.min_le_padicValRat_add twice: once to z + (-r) = q and once to z + (-q) = r. Rewrite with padicValRat.neg, and note that 0 ≤ padicValRat p z via padicValRat.of_int + Nat.cast_nonneg. Then omega closes everything (it handles min and ℕ→ℤ casts). You never need z ≠ 0, since padicValRat p 0 = 0 and the lemma only needs the SUM to be nonzero. padicValRat.add_eq_of_lt gives v(y - x) = min when v x ≠ v y. Used for IMO 2018 P5 (eventually constant sequence) with the potential Φ(v) = if v < α then 1 else v - α summed over primes. The sum is a nonincreasing ℕ sequence, so Nat.find on its values gives the stabilization point.