diff --git a/Analysis/Section_5_4.lean b/Analysis/Section_5_4.lean
index b0b61759..9212888c 100644
--- a/Analysis/Section_5_4.lean
+++ b/Analysis/Section_5_4.lean
@@ -26,39 +26,39 @@ Users of the companion who have completed the exercises in this section are welc
 namespace Chapter5
 
 /--
-  Definition 5.4.1 (sequences bounded away from zero with sign). Sequences are indexed to start
-  from zero as this is more convenient for Mathlib purposes.
+  Definition 5.4.1 (sequences bounded away from zero with sign) (positive). Sequences are indexed
+  to start from zero as this is more convenient for Mathlib purposes.
 -/
 abbrev BoundedAwayPos (a:ℕ → ℚ) : Prop :=
   ∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≥ c
 
-/-- Definition 5.4.1 (sequences bounded away from zero with sign). -/
+/-- Definition 5.4.1 (sequences bounded away from zero with sign) (negative). -/
 abbrev BoundedAwayNeg (a:ℕ → ℚ) : Prop :=
   ∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≤ -c
 
-/-- Definition 5.4.1 (sequences bounded away from zero with sign). -/
+/-- Definition 5.4.1 (sequences bounded away from zero with sign) (positive, unfolded). -/
 theorem boundedAwayPos_def (a:ℕ → ℚ) : BoundedAwayPos a ↔ ∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≥ c := by
   rfl
 
-/-- Definition 5.4.1 (sequences bounded away from zero with sign). -/
+/-- Definition 5.4.1 (sequences bounded away from zero with sign) (negative, unfolded). -/
 theorem boundedAwayNeg_def (a:ℕ → ℚ) : BoundedAwayNeg a ↔ ∃ (c:ℚ), c > 0 ∧ ∀ n, a n ≤ -c := by
   rfl
 
-/-- Examples 5.4.2 -/
+/-- Examples 5.4.2 (strictly positive) -/
 example : BoundedAwayPos (fun n ↦ 1 + 10^(-(n:ℤ)-1)) := ⟨ 1, by norm_num, by intros; simp; positivity ⟩
 
-/-- Examples 5.4.2 -/
+/-- Examples 5.4.2 (strictly negative) -/
 example : BoundedAwayNeg (fun n ↦ -1 - 10^(-(n:ℤ)-1)) := ⟨ 1, by norm_num, by intros; simp; positivity ⟩
 
-/-- Examples 5.4.2 -/
+/-- Examples 5.4.2 (alternating, not positive) -/
 example : ¬ BoundedAwayPos (fun n ↦ (-1)^n) := by
   intro ⟨ c, h1, h2 ⟩; specialize h2 1; grind
 
-/-- Examples 5.4.2 -/
+/-- Examples 5.4.2 (alternating, not negative) -/
 example : ¬ BoundedAwayNeg (fun n ↦ (-1)^n) := by
   intro ⟨ c, h1, h2 ⟩; specialize h2 0; grind
 
-/-- Examples 5.4.2 -/
+/-- Examples 5.4.2 (alternating, bounded away from zero) -/
 example : BoundedAwayZero (fun n ↦ (-1)^n) := ⟨ 1, by norm_num, by intros; simp ⟩
 
 theorem BoundedAwayZero.boundedAwayPos {a:ℕ → ℚ} (ha: BoundedAwayPos a) : BoundedAwayZero a := by
@@ -82,34 +82,34 @@ theorem Real.isPos_def (x:Real) :
 theorem Real.isNeg_def (x:Real) :
     IsNeg x ↔ ∃ a:ℕ → ℚ, BoundedAwayNeg a ∧ (a:Sequence).IsCauchy ∧ x = LIM a := by rfl
 
-/-- Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1 -/
+/-- Proposition 5.4.4 (trichotomy, at least one) / Exercise 5.4.1 -/
 theorem Real.trichotomous (x:Real) : x = 0 ∨ x.IsPos ∨ x.IsNeg := by sorry
 
-/-- Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1 -/
+/-- Proposition 5.4.4 (trichotomy, zero/positive exclusive) / Exercise 5.4.1 -/
 theorem Real.not_zero_pos (x:Real) : ¬(x = 0 ∧ x.IsPos) := by sorry
 
 theorem Real.nonzero_of_pos {x:Real} (hx: x.IsPos) : x ≠ 0 := by
   have := not_zero_pos x
   simpa [hx] using this
 
-/-- Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1 -/
+/-- Proposition 5.4.4 (trichotomy, zero/negative exclusive) / Exercise 5.4.1 -/
 theorem Real.not_zero_neg (x:Real) : ¬(x = 0 ∧ x.IsNeg) := by sorry
 
 theorem Real.nonzero_of_neg {x:Real} (hx: x.IsNeg) : x ≠ 0 := by
   have := not_zero_neg x
   simpa [hx] using this
 
-/-- Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1 -/
+/-- Proposition 5.4.4 (trichotomy, positive/negative exclusive) / Exercise 5.4.1 -/
 theorem Real.not_pos_neg (x:Real) : ¬(x.IsPos ∧ x.IsNeg) := by sorry
 
-/-- Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1 -/
+/-- Proposition 5.4.4 (negation) / Exercise 5.4.1 -/
 @[simp]
 theorem Real.neg_iff_pos_of_neg (x:Real) : x.IsNeg ↔ (-x).IsPos := by sorry
 
-/-- Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1 -/
+/-- Proposition 5.4.4 (sum) / Exercise 5.4.1 -/
 theorem Real.pos_add {x y:Real} (hx: x.IsPos) (hy: y.IsPos) : (x+y).IsPos := by sorry
 
-/-- Proposition 5.4.4 (basic properties of positive reals) / Exercise 5.4.1 -/
+/-- Proposition 5.4.4 (product) / Exercise 5.4.1 -/
 theorem Real.pos_mul {x y:Real} (hx: x.IsPos) (hy: y.IsPos) : (x*y).IsPos := by sorry
 
 theorem Real.pos_of_coe (q:ℚ) : (q:Real).IsPos ↔ q > 0 := by sorry
@@ -120,29 +120,29 @@ open Classical in
 /-- Need to use classical logic here because {name}`IsPos` and {name}`IsNeg` are not decidable -/
 noncomputable abbrev Real.abs (x:Real) : Real := if x.IsPos then x else (if x.IsNeg then -x else 0)
 
-/-- Definition 5.4.5 (absolute value) -/
+/-- Definition 5.4.5 (absolute value) (positive case) -/
 @[simp]
 theorem Real.abs_of_pos (x:Real) (hx: x.IsPos) : abs x = x := by
   simp [abs, hx]
 
-/-- Definition 5.4.5 (absolute value) -/
+/-- Definition 5.4.5 (absolute value) (negative case) -/
 @[simp]
 theorem Real.abs_of_neg (x:Real) (hx: x.IsNeg) : abs x = -x := by
   have : ¬x.IsPos := by have := not_pos_neg x; simpa [hx] using this
   simp [abs, hx, this]
 
-/-- Definition 5.4.5 (absolute value) -/
+/-- Definition 5.4.5 (absolute value) (zero case) -/
 @[simp]
 theorem Real.abs_of_zero : abs 0 = 0 := by
   have hpos: ¬(0:Real).IsPos := by have := not_zero_pos 0; simpa using this
   have hneg: ¬(0:Real).IsNeg := by have := not_zero_neg 0; simpa using this
   simp [abs, hpos, hneg]
 
-/-- Definition 5.4.6 (Ordering of the reals) -/
+/-- Definition 5.4.6 (Ordering of the reals) (strict order) -/
 instance Real.instLT : LT Real where
   lt x y := (x-y).IsNeg
 
-/-- Definition 5.4.6 (Ordering of the reals) -/
+/-- Definition 5.4.6 (Ordering of the reals) (order) -/
 instance Real.instLE : LE Real where
   le x y := (x < y) ∨ (x = y)
 
@@ -159,16 +159,16 @@ theorem Real.gt_of_coe (q q':ℚ): q > q' ↔ (q:Real) > (q':Real) := Real.lt_of
 theorem Real.isPos_iff (x:Real) : x.IsPos ↔ x > 0 := by sorry
 theorem Real.isNeg_iff (x:Real) : x.IsNeg ↔ x < 0 := by sorry
 
-/-- Proposition 5.4.7(a) (order trichotomy) / Exercise 5.4.2 -/
+/-- Proposition 5.4.7(a) (order trichotomy) (at least one holds) / Exercise 5.4.2 -/
 theorem Real.trichotomous' (x y:Real) : x > y ∨ x < y ∨ x = y := by sorry
 
-/-- Proposition 5.4.7(a) (order trichotomy) / Exercise 5.4.2 -/
+/-- Proposition 5.4.7(a) (order trichotomy) (> and < exclusive) / Exercise 5.4.2 -/
 theorem Real.not_gt_and_lt (x y:Real) : ¬ (x > y ∧ x < y):= by sorry
 
-/-- Proposition 5.4.7(a) (order trichotomy) / Exercise 5.4.2 -/
+/-- Proposition 5.4.7(a) (order trichotomy) (> and = exclusive) / Exercise 5.4.2 -/
 theorem Real.not_gt_and_eq (x y:Real) : ¬ (x > y ∧ x = y):= by sorry
 
-/-- Proposition 5.4.7(a) (order trichotomy) / Exercise 5.4.2 -/
+/-- Proposition 5.4.7(a) (order trichotomy) (< and = exclusive) / Exercise 5.4.2 -/
 theorem Real.not_lt_and_eq (x y:Real) : ¬ (x < y ∧ x = y):= by sorry
 
 /-- Proposition 5.4.7(b) (order is anti-symmetric) / Exercise 5.4.2 -/
@@ -180,11 +180,11 @@ theorem Real.lt_trans {x y z:Real} (hxy: x < y) (hyz: y < z) : x < z := by sorry
 /-- Proposition 5.4.7(d) (addition preserves order) / Exercise 5.4.2 -/
 theorem Real.add_lt_add_right {x y:Real} (z:Real) (hxy: x < y) : x + z < y + z := by sorry
 
-/-- Proposition 5.4.7(e) (positive multiplication preserves order) / Exercise 5.4.2 -/
+/-- Proposition 5.4.7(e) (positive multiplication preserves order) (strict) / Exercise 5.4.2 -/
 theorem Real.mul_lt_mul_right {x y z:Real} (hxy: x < y) (hz: z.IsPos) : x * z < y * z := by
   rw [antisymm, gt_iff] at hxy ⊢; convert pos_mul hxy hz using 1; ring
 
-/-- Proposition 5.4.7(e) (positive multiplication preserves order) / Exercise 5.4.2 -/
+/-- Proposition 5.4.7(e) (positive multiplication preserves order) (non-strict) / Exercise 5.4.2 -/
 theorem Real.mul_le_mul_left {x y z:Real} (hxy: x ≤ y) (hz: z.IsPos) : z * x ≤ z * y := by sorry
 
 theorem Real.mul_pos_neg {x y:Real} (hx: x.IsPos) (hy: y.IsNeg) : (x * y).IsNeg := by
@@ -353,43 +353,43 @@ theorem Real.max_eq (x y:Real) : max x y = if x ≥ y then x else y := max_def'
 
 theorem Real.min_eq (x y:Real) : min x y = if x ≤ y then x else y := rfl
 
-/-- Exercise 5.4.9 (a) -/
+/-- Exercise 5.4.9 (i) (max as negated min) -/
 theorem Real.neg_max (x y:Real) : max x y = - min (-x) (-y) := by sorry
 
-/-- Exercise 5.4.9 (b) -/
+/-- Exercise 5.4.9 (i) (min as negated max) -/
 theorem Real.neg_min (x y:Real) : min x y = - max (-x) (-y) := by sorry
 
-/-- Exercise 5.4.9 (c) -/
+/-- Exercise 5.4.9 (ii) (commutativity of max) -/
 theorem Real.max_comm (x y:Real) : max x y = max y x := by sorry
 
-/-- Exercise 5.4.9 (d) -/
+/-- Exercise 5.4.9 (ii) (idempotence of max) -/
 theorem Real.max_self (x:Real) : max x x = x := by sorry
 
-/-- Exercise 5.4.9 (e) -/
+/-- Exercise 5.4.9 (ii) (translation of max) -/
 theorem Real.max_add (x y z:Real) : max (x + z) (y + z) = max x y + z := by sorry
 
-/-- Exercise 5.4.9 (f) -/
+/-- Exercise 5.4.9 (ii) (positive scaling of max) -/
 theorem Real.max_mul (x y :Real) {z:Real} (hz: z.IsPos) : max (x * z) (y * z) = max x y * z := by
   sorry
-/- Additional exercise (after 5.4.9 (f)): What happens if z is negative? -/
+/- Additional exercise (after 5.4.9 (ii)): What happens if z is negative? -/
 
-/-- Exercise 5.4.9 (g) -/
+/-- Exercise 5.4.9 (iii) (commutativity of min) -/
 theorem Real.min_comm (x y:Real) : min x y = min y x := by sorry
 
-/-- Exercise 5.4.9 (h) -/
+/-- Exercise 5.4.9 (iii) (idempotence of min) -/
 theorem Real.min_self (x:Real) : min x x = x := by sorry
 
-/-- Exercise 5.4.9 (i) -/
+/-- Exercise 5.4.9 (iii) (translation of min) -/
 theorem Real.min_add (x y z:Real) : min (x + z) (y + z) = min x y + z := by sorry
 
-/-- Exercise 5.4.9 (j) -/
+/-- Exercise 5.4.9 (iii) (positive scaling of min) -/
 theorem Real.min_mul (x y :Real) {z:Real} (hz: z.IsPos) : min (x * z) (y * z) = min x y * z := by
   sorry
 
-/-- Exercise 5.4.9 (k) -/
+/-- Exercise 5.4.9 (iv) (inverse of max) -/
 theorem Real.inv_max {x y :Real} (hx:x.IsPos) (hy:y.IsPos) : (max x y)⁻¹ = min x⁻¹ y⁻¹ := by sorry
 
-/-- Exercise 5.4.9 (l) -/
+/-- Exercise 5.4.9 (iv) (inverse of min) -/
 theorem Real.inv_min {x y :Real} (hx:x.IsPos) (hy:y.IsPos) : (min x y)⁻¹ = max x⁻¹ y⁻¹ := by sorry
 
 /-- Not from textbook: the rationals map as an ordered ring homomorphism into the reals. -/