Olympiad 'xy is a square' arguments in Lean: odd p-adic valuation ⇒ p ∣ y

Reusable lemma for FE/NT problems like IMO 2010 P3. If IsSquare (x*y), x = p^(2j+1)*u with ¬p ∣ u, and y > 0, then p ∣ y. Proof: by_contra, obtain ⟨t, ht⟩ := hsq, congrArg (padicValNat p) ht, then rw with padicValNat.mul (needs ≠ 0 side goals and Fact p.Prime), padicValNat.prime_pow, and padicValNat.eq_zero_of_not_dvd twice; omega closes 2j+1 = 2v. To force odd valuations, choose n with g(k)+n = p·D or p³·D, where D = p·(g k + g l) + 1 is coprime to p. Keep D opaque via obtain ⟨D, hD⟩ : ∃ D, D = _ := ⟨_, rfl⟩, because set lets rw [mul_add] unfold into D and produces huge omega atoms. Witness equations such as g l + (p^3*D - g k) = p^(2*0+1)*(p^2*D + a) go through as rw [show p^(2*0+1)*(p^2*D+a) = p^3*D + p*a by ring]; omega. Turning '|d| ≠ 1' into a prime factor: Nat.exists_prime_and_dvd (h : d.natAbs ≠ 1) plus Int.natCast_dvd.2.