theorem Rat.between_int (x : ℚ) : ∃! n : ℤ, ↑n ≤ x ∧ x < ↑n + 1

Proposition 4.4.1 (Interspersing of integers by rationals) / Exercise 4.4.1

theorem Nat.exists_gt (x : ℚ) : ∃ (n : ℕ), ↑n > x

theorem Rat.exists_between_rat {x y : ℚ} (h : x < y) : ∃ (z : ℚ), x < z ∧ z < y

Proposition 4.4.3 (Interspersing of rationals)

theorem Nat.no_infinite_descent : ¬∃ (a : ℕ → ℕ), ∀ (n : ℕ), a (n + 1) < a n

Exercise 4.4.2 (a)

def Int.infinite_descent : Decidable (∃ (a : ℕ → ℤ), ∀ (n : ℕ), a (n + 1) < a n)

Exercise 4.4.2 (b)

Equations

• Int.infinite_descent = sorry

def Rat.pos_infinite_descent : Decidable (∃ (a : ℕ → { x : ℚ // 0 < x }), ∀ (n : ℕ), a (n + 1) < a n)

Exercise 4.4.2 (b')

Equations

• Rat.pos_infinite_descent = sorry

theorem Nat.even_or_odd'' (n : ℕ) : Even n ∨ Odd n

theorem Nat.not_even_and_odd (n : ℕ) : ¬(Even n ∧ Odd n)

theorem Rat.not_exist_sqrt_two : ¬∃ (x : ℚ), x ^ 2 = 2

Proposition 4.4.4 / Exercise 4.4.3

theorem Rat.exist_approx_sqrt_two {ε : ℚ} (hε : ε > 0) : ∃ x ≥ 0, x ^ 2 < 2 ∧ 2 < (x + ε) ^ 2

Proposition 4.4.5