theorem AlgebraicIntegers.ideal_le_maximal {R : Type u_1} [CommRing R] [Nontrivial R] [IsNoetherianRing R] (I : Ideal R) (hI : I ≠ ⊤) : ∃ (M : Ideal R), M.IsMaximal ∧ I ≤ M