∀ {R : Type u_1} [inst : CommRing R] {p : Ideal R} {n : ℕ} [p.IsPrime] [IsNoetherianRing R],
  p.height ≤ ↑n ↔ ∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < ↑n