diff --git a/analysis/Analysis/Section_4_4.lean b/analysis/Analysis/Section_4_4.lean
index 87328cb1..769e8cde 100644
--- a/analysis/Analysis/Section_4_4.lean
+++ b/analysis/Analysis/Section_4_4.lean
@@ -44,14 +44,20 @@ theorem Rat.exists_between_rat {x y:ℚ} (h: x < y) : ∃ z:ℚ, x < z ∧ z < y
   . convert add_lt_add_right h' (x/2) using 1 <;> ring
   convert add_lt_add_right h' (y/2) using 1 <;> ring
 
-/-- Exercise 4.4.2 -/
+/-- Exercise 4.4.2 (a) -/
 theorem Nat.no_infinite_descent : ¬ ∃ a:ℕ → ℕ, ∀ n, a (n+1) < a n := by
   sorry
 
+/-- Exercise 4.4.2 (b) -/
 def Int.infinite_descent : Decidable (∃ a:ℕ → ℤ, ∀ n, a (n+1) < a n) := by
   -- the first line of this construction should be either `apply isTrue` or `apply isFalse`.
   sorry
 
+/-- Exercise 4.4.2 (b) -/
+def Rat.pos_infinite_descent : Decidable (∃ a:ℕ → {x: ℚ // 0 < x}, ∀ n, a (n+1) < a n) := by
+  -- the first line of this construction should be either `apply isTrue` or `apply isFalse`.
+  sorry
+
 #check even_iff_exists_two_mul
 #check odd_iff_exists_bit1