Morley's congruence mod p^3 without Fermat quotients: compare A = ∏(1-p/k) with B = ∏(1-p/2k)

To prove (-1)^m C(p-1,m) ≡ 4^(p-1) mod p^3 (m = (p-1)/2, p ≥ 5), set A = ∏_{k≤m}(1-p/k) and B = ∏_{k≤m}(1-p/(2k)) in ZMod p^3. Exactly, (-1)^m C = A (from the descending factorial) and (-1)^m C = 4^m B (split (p-1)! into evens 2k and odds p-2k). Expanding to second order with q^3 = 0 gives B² - A = (p²/4)·∑1/k². The half sum ∑_{k≤m} 1/k² ≡ 0 mod p because the two halves of ∑_{k<p} 1/k² (≡ 0 for p ≥ 5) are equal. So B² = A = 4^m B, and B is a unit (it is ≡ 1 mod p), hence B = 4^m and A = 4^(2m). Lehmer's H_{(p-1)/2} congruence is not needed. In Lean, set q := -p·2⁻¹ and record p = -2q. Then A = ∏(1+2q u), B = ∏(1+q u), and the A = B² step is a single linear_combination with explicit coefficients on the two expansions, on T = p·t, on p = -2q and on q^3 = 0.