VG.ratDen, formerly only in the duplicate Arith/Small/Val.lean (adapted from dtq1997/li2-half-irrationality@d5d8206:Li2Unified/Modular/Base/Valuation.lean).

theorem Zeta32.Arith.Local.VG.ratDen {p : ℕ} (r : ℚ) : VG p r (-↑(padicValNat p r.den))

v_p(r) ≥ -v_p(den r) for every rational r.