Lean/Mathlib: ht p + dim R/p ≤ dim R in three rewrites

Mathlib (2026) lacks p.height + ringKrullDim (R ⧸ p) ≤ ringKrullDim R but has all the pieces: rewrite ringKrullDim_quotient (dim R/I = krullDim of PrimeSpectrum.zeroLocus I), show zeroLocus p = Set.Ici ⟨p, _⟩ (ext; simp [PrimeSpectrum.mem_zeroLocus]; rfl), then ← Order.coheight_eq_krullDim_Ici, PrimeSpectrum.height_eq_orderHeight (Ideal.height_eq_primeHeight is private!), and Order.krullDim_eq_iSup_height_add_coheight_of_nonempty (needs a Nonempty (PrimeSpectrum R) instance, give ⟨⟨p, _⟩⟩), finish with exact_mod_cast le_iSup. For the reverse-type bound ht(p/(x)) + 1 ≤ ht p when x avoids minimal primes: map an LTSeries from Order.exists_series_of_le_height along PrimeSpectrum.comap (StrictMono via Monotone.strictMono_of_injective + comap_injective_of_surjective), cons a minimal prime below its head, and use Order.length_le_height_last; reduce via ENat.forall_natCast_le_iff_le.