Exhibit infinite descents in ℤ and positive ℚ

Analysis/Section_4_4.lean

@@ -50,13 +50,24 @@ theorem Nat.no_infinite_descent : ¬ ∃ a:ℕ → ℕ, ∀ n, a (n+1) < a n :=
 
 /-- 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
+  apply isTrue
+  refine ⟨fun n ↦ - (n:ℤ), ?_⟩
+  intro n
+  -- simp closes -(n+1) < -n
+  simp
 
 /-- 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
+  apply isTrue
+  refine ⟨fun n ↦ ⟨(1 : ℚ) / (n + 1), by positivity⟩, ?_⟩
+  intro n
+  simp only [Subtype.mk_lt_mk]
+  -- goal: 1 / (↑(n + 1) + 1) < 1 / (↑n + 1)
+  have h1 : (0 : ℚ) < (n : ℚ) + 1 := by positivity
+  have h2 : (0 : ℚ) < ((n + 1 : ℕ) : ℚ) + 1 := by positivity
+  rw [div_lt_div_iff₀ h2 h1]
+  push_cast
+  linarith
 
 #check even_iff_exists_two_mul
 #check odd_iff_exists_bit1