diff --git a/CommAlg/grant2.lean b/CommAlg/grant2.lean
index 24edcff..8bf6085 100644
--- a/CommAlg/grant2.lean
+++ b/CommAlg/grant2.lean
@@ -55,10 +55,14 @@ def symbolicIdeal(Q : Ideal R) {hin : Q.IsPrime} (I : Ideal R) : Ideal R where
     exact Ideal.mul_mem_left _ _ hs2
 
 
-theorem WF_interval_le_prime (I : Ideal R) (P : Ideal R) [P.IsPrime] 
+theorem WF_interval_le_prime [IsNoetherianRing R] (I : Ideal R) (P : Ideal R) [P.IsPrime] 
   (h : ∀ J ∈ (Set.Icc I P), J.IsPrime → J = P ):
   WellFounded ((· < ·) : (Set.Icc I P) → (Set.Icc I P) → Prop ) := sorry 
 
+theorem WF_interval_of_no_primes [IsNoetherianRing R] (I : Ideal R) (J : Ideal R)
+  (h : ∀ K ∈ (Set.Icc I J), ¬ K.IsPrime) :
+  WellFounded ((· < ·) : (Set.Icc I J) → (Set.Icc I J) → Prop ) := sorry
+
 protected lemma LocalRing.height_le_one_of_minimal_over_principle
   [LocalRing R] {x : R} 
   (h : (closedPoint R).asIdeal ∈ (Ideal.span {x}).minimalPrimes) :