Chap6.qmd

# Mathematical Induction

## 6.1.  Proof by Mathematical Induction

Section 6.1 of *HTPI* introduces a new proof technique called *mathematical induction*.  It is used for proving statements of the form `∀ (n : Nat), P n`.  Here is how it works (*HTPI* p. 273):

#### To prove a goal of the form `∀ (n : Nat), P n`:

::: {.ind}
First prove `P 0`, and then prove `∀ (n : Nat), P n → P (n + 1)`.  The first of these proofs is sometimes called the *base case* and the second the *induction step*.
:::

For an explanation of why this strategy works to establish the truth of `∀ (n : Nat), P n`, see *HTPI*.  Here we focus on using mathematical induction in Lean.

To use mathematical induction in a Lean proof, we will use the tactic `by_induc`.  If the goal has the form `∀ (n : Nat), P n`, then the `by_induc` tactic leaves the list of givens unchanged, but it replaces the goal with the goals for the base case and induction step.  Thus, the effect of the tactic can be summarized as follows:

::: {.lftrt}
::: {.bef}
```state
>> ⋮
⊢ ∀ (n : Nat), P n
```
:::

::: {.aft}
```state
case Base_Case
>> ⋮
⊢ P 0
case Induction_Step
>> ⋮
⊢ ∀ (n : Nat), P n → P (n + 1)
```
:::
:::

To illustrate proof by mathematical induction in Lean, we turn first to Example 6.1.2 in *HTPI*, which gives a proof of the statement $\forall n \in \mathbb{N} (3 \mid (n^3 - n))$.  For reasons that we will explain a little later, we will prove a slightly different theorem:  $\forall n \in \mathbb{N} (3 \mid (n^3 + 2n))$.  Here is a proof of the theorem, modeled on the proof in Example 6.1.2 of *HTPI* (*HTPI* pp. 276--277).

::: {.thm}
For every natural number $n$, $3 \mid (n^3 + 2n)$.
:::

::: {.proof}
We use mathematical induction.

Base Case:  If $n = 0$, then $n^3 + 2n = 0 = 3 \cdot 0$, so $3 \mid (n^3 + 2n)$.

Induction Step:  Let $n$ be an arbitrary natural number and suppose $3 \mid (n^3 + 2n)$.  Then we can choose an integer $k$ such that $3k = n^3 + 2n$.  Thus,
\begin{align*}
(n+1)^3 + 2(n+1) &= n^3 + 3n^2 + 3n + 1 + 2n + 2\\
&= (n^3 + 2n) + 3n^2 + 3n + 3\\
&= 3k + 3n^2 + 3n + 3\\
&= 3(k + n^2 + n + 1).
\end{align*}
Therefore $3 \mid ((n+1)^3 + 2(n+1))$, as required. [ □]{.excl}\qedhere
:::

Now let's try writing the same proof in Lean.  We start, of course, with the `by_induc` tactic.

::: {.inout}
::: {.inpt}
```lean
theorem Like_Example_6_1_2 :
    ∀ (n : Nat), 3 ∣ n ^ 3 + 2 * n := by
  by_induc
  **done::
```
:::

::: {.outpt}
```state
case Base_Case
⊢ 3 ∣ 0 ^ 3 + 2 * 0
case Induction_Step
⊢ ∀ (n : ℕ),
>>  3 ∣ n ^ 3 + 2 * n →
>>  3 ∣ (n + 1) ^ 3 +
>>      2 * (n + 1)
```
:::
:::

The base case is easy:  The `define` tactic tells us that the goal means `∃ (c : Nat), 0 ^ 3 + 2 * 0 = 3 * c`, and then `apply Exists.intro 0` changes the goal to `0 ^ 3 + 2 * 0 = 3 * 0`.  Both sides are definitionally equal to `0`, so `rfl` finishes off the base case.  For the induction step, we begin, as in the *HTPI* proof, by introducing an arbitrary natural number `n` and assuming `3 ∣ n ^ 3 + 2 * n`.  This assumption is called the *inductive hypothesis*, so in the Lean proof we give it the identifier `ih`.  Our goal now is to prove `3 ∣ (n + 1) ^ 3 + 2 * (n + 1)`.

::: {.inout}
::: {.inpt}
```lean
theorem Like_Example_6_1_2 :
    ∀ (n : Nat), 3 ∣ n ^ 3 + 2 * n := by
  by_induc
  · -- Base Case
    define
    apply Exists.intro 0
    rfl
    done
  · -- Induction Step
    fix n : Nat
    assume ih : 3 ∣ n ^ 3 + 2 * n
    **done::
  done
```
:::

::: {.outpt}
```state
case Induction_Step
n : ℕ
ih : 3 ∣ n ^ 3 + 2 * n
⊢ 3 ∣ (n + 1) ^ 3 +
>>      2 * (n + 1)
```
:::
:::

The rest of the Lean proof follows the model of the *HTPI* proof:  we use the inductive hypothesis to introduce a `k` such that `n ^ 3 + 2 * n = 3 * k`, and then we use a calculational proof to show that `(n + 1) ^ 3 + 2 * (n + 1) = 3 * (k + n ^ 2 + n + 1)`.

```lean
theorem Like_Example_6_1_2 :
    ∀ (n : Nat), 3 ∣ n ^ 3 + 2 * n := by
  by_induc
  · -- Base Case
    define         --Goal : ∃ (c : Nat), 0 ^ 3 + 2 * 0 = 3 * c
    apply Exists.intro 0
    rfl
    done
  · -- Induction Step
    fix n : Nat
    assume ih : 3 ∣ n ^ 3 + 2 * n
    define at ih   --ih : ∃ (c : Nat), n ^ 3 + 2 * n = 3 * c
    obtain (k : Nat) (h1 : n ^ 3 + 2 * n = 3 * k) from ih
    define         --Goal : ∃ (c : Nat), (n + 1) ^ 3 + 2 * (n + 1) = 3 * c
    apply Exists.intro (k + n ^ 2 + n + 1)
    show (n + 1) ^ 3 + 2 * (n + 1) = 3 * (k + n ^ 2 + n + 1) from
      calc (n + 1) ^ 3 + 2 * (n + 1)
        _ = n ^ 3 + 2 * n + 3 * n ^ 2 + 3 * n + 3 := by ring
        _ = 3 * k + 3 * n ^ 2 + 3 * n + 3 := by rw [h1]
        _ = 3 * (k + n ^ 2 + n + 1) := by ring
    done
  done
```

Next we'll look at Example 6.1.1 in *HTPI*, which proves that for every natural number $n$, $2^0 + 2^1 + \cdots + 2^n = 2^{n+1} - 1$.  Once again, we will change the theorem slightly before proving it in Lean.  What we will prove is that for every $n$, $(2^0 + 2^1 + \cdots + 2^n) + 1 = 2^{n+1}$.  To understand this theorem you must be able to recognize what the "$\cdots$" stands for.  A human reader will probably realize that the numbers being added up here are the numbers of the form $2^i$, where $i$ runs through all of the natural numbers from 0 to $n$.  But Lean can't be expected to figure out this pattern, so we must be more explicit.

Section 6.3 of *HTPI* introduces the explicit notation that mathematicians usually use for such sums.  If $f$ is a function whose domain is the natural numbers, then
$$
\sum_{i=0}^n f(i) = f(0) + f(1) + \cdots + f(n).
$$
More generally, if $k \le n$ then
$$
\sum_{i=k}^n f(i) = f(k) + f(k+1) + \cdots + f(n).
$$

The notation we will use in Lean for this sum is `Sum i from k to n, f i`.  Thus, a mathematician would state our theorem like this:

::: {.thm}
For every natural number $n$,
$$
\left(\sum_{i=0}^n 2^i\right) + 1 = 2^{n+1}.
$$
:::

And to state the same theorem in Lean, we will write:

```lean
theorem Like_Example_6_1_1 :
    ∀ (n : Nat), (Sum i from 0 to n, 2 ^ i) + 1 = 2 ^ (n + 1)
```

We will have more to say later about how the notation `Sum i from k to n, f i` is defined.  But to use the notation in a proof, we will just need to know a few theorems.  The `#check` command will tell us the meanings of the theorems `sum_base`, `sum_step`, and `sum_from_zero_step`:

::: {.ind}
```
@sum_base : ∀ {A : Type} [inst : AddZeroClass A] {k : ℕ} {f : ℕ → A},
            Sum i from k to k, f i = f k

@sum_step : ∀ {A : Type} [inst : AddZeroClass A] {k n : ℕ} {f : ℕ → A},
            k ≤ n → Sum i from k to n + 1, f i =
              (Sum i from k to n, f i) + f (n + 1)

@sum_from_zero_step :
            ∀ {A : Type} [inst : AddZeroClass A] {n : ℕ} {f : ℕ → A},
            Sum i from 0 to n + 1, f i =
              (Sum i from 0 to n, f i) + f (n + 1)
```
:::

As usual, we don't need to pay too much attention to the implicit arguments in the first line of each statement.  What is important is that `sum_base` can be used to prove any statement of the form

::: {.ind}
```
Sum i from k to k, f i = f k
```
:::

and `sum_step` proves any statement of the form

::: {.ind}
```
k ≤ n → Sum i from k to n + 1, f i = (Sum i from k to n, f i) + f (n + 1).
```
:::

In the case `k = 0`, we have the simpler theorem `sum_from_zero_step`, which proves

::: {.ind}
```
Sum i from 0 to n + 1, f i = (Sum i from 0 to n, f i) + f (n + 1).
```
:::

With that preparation, we can start on the proof.  Once again we begin with the `by_induc` tactic.  Our goal for the base case is `(Sum i from 0 to 0, 2 ^ i) + 1 = 2 ^ (0 + 1)`.  To deal with the term `Sum i from 0 to 0, 2 ^ i`, we use that fact that `sum_base` proves `Sum i from 0 to 0, 2 ^ i = 2 ^ 0`.  It follows that the tactic `rewrite [sum_base]` will change the goal to `2 ^ 0 + 1 = 2 ^ (0 + 1)`.  Of course, this means `2 = 2`, so `rfl` finishes the base case.  For the induction step, we start by introducing an arbitrary natural number `n` and assuming the inductive hypothesis.

```lean
theorem Like_Example_6_1_1 :
    ∀ (n : Nat), (Sum i from 0 to n, 2 ^ i) + 1 = 2 ^ (n + 1) := by
  by_induc
  · -- Base Case
    rewrite [sum_base]
    rfl
    done
  · -- Induction Step
    fix n : Nat
    assume ih : (Sum i from 0 to n, 2 ^ i) + 1 = 2 ^ (n + 1)
    **done::
  done
```

Our goal is now `(Sum i from 0 to n + 1, 2 ^ i) + 1 = 2 ^ (n + 1 + 1)`, and we use a calculational proof to prove this.  Often the key to the proof of the induction step is to find a relationship between the inductive hypothesis and the goal.  In this case, that means finding a relationship between `Sum i from 0 to n, 2 ^ i` and `Sum i from 0 to n + 1, 2 ^ i`.  The relationship we need is given by the theorem `sum_from_zero_step`.  The tactic `rewrite [sum_from_zero_step]` will replace `Sum i from 0 to n + 1, 2 ^ i` with `(Sum i from 0 to n, 2 ^ i) + 2 ^ (n + 1)`.  The rest of the calculation proof involves straightforward algebra, handled by the `ring` tactic, together with an application of the inductive hypothesis.

```lean
theorem Like_Example_6_1_1 :
    ∀ (n : Nat), (Sum i from 0 to n, 2 ^ i) + 1 = 2 ^ (n + 1) := by
  by_induc
  · -- Base Case
    rewrite [sum_base]
    rfl
    done
  · -- Induction Step
    fix n : Nat
    assume ih : (Sum i from 0 to n, 2 ^ i) + 1 = 2 ^ (n + 1)
    show (Sum i from 0 to n + 1, 2 ^ i) + 1 = 2 ^ (n + 1 + 1) from
      calc (Sum i from 0 to n + 1, 2 ^ i) + 1
        _ = (Sum i from 0 to n, 2 ^ i) + 2 ^ (n + 1) + 1 := by
              rw [sum_from_zero_step]
        _ = (Sum i from 0 to n, 2 ^ i) + 1 + 2 ^ (n + 1) := by ring
        _ = 2 ^ (n + 1) + 2 ^ (n + 1) := by rw [ih]
        _ = 2 ^ (n + 1 + 1) := by ring
    done
  done
```

The last example in Section 6.1 of *HTPI* gives a proof of the statement $\forall n \ge 5 (2^n > n^2)$.  The proof is by mathematical induction, but since we are only interested in natural numbers greater than or equal to 5, it uses 5 in the base case instead of 0.  Here are the theorem and proof from *HTPI* (*HTPI* p. 278):

::: {.thm}
For every natural number $n \ge 5$, $2^n > n^2$.
:::

::: {.proof}
By mathematical induction.

Base case:  When $n = 5$ we have $2^n = 32 > 25 = n^2$.

Induction step:  Let $n \ge 5$ be arbitrary, and suppose that $2^n > n^2$.  Then
\begin{align*}
2^{n+1} &= 2 \cdot 2^n\\
&> 2n^2 &&\text{(inductive hypothesis)}\\
&= n^2 + n^2\\
&\ge n^2 + 5n &&\text{(since $n \ge 5$)}\\
&= n^2 + 2n + 3n\\
&> n^2 + 2n + 1 = (n+1)^2. &&\Box
\end{align*}
\renewcommand{\qed}{}
:::

Notice that the sequence of calculations at the end of the proof mixes $=$, $>$, and $\ge$ in a way that establishes the final conclusion $2^{n+1} > (n+1)^2$.  As we'll see, such a mixture is allowed in calculational proofs in Lean as well.

To write this proof in Lean, there is no need to specify that the base case should be `n = 5`; the `by_induc` tactic is smart enough to figure that out on its own, as you can see in the tactic state below.  (Notice that, as in *HTPI*, in Lean we can write `∀ n ≥ k, P n` as an abbreviation for `∀ (n : Nat), n ≥ k → P n`.)

::: {.inout}
::: {.inpt}
```lean
theorem Example_6_1_3 :
    ∀ n ≥ 5, 2 ^ n > n ^ 2 := by
  by_induc
  **done::
```
:::

::: {.outpt}
```state
case Base_Case
⊢ 2 ^ 5 > 5 ^ 2
case Induction_Step
⊢ ∀ n ≥ 5,
>>  2 ^ n > n ^ 2 →
>>  2 ^ (n + 1) >
>>      (n + 1) ^ 2
```
:::
:::

To complete this proof we'll use two tactics we haven't used before: `decide` and `linarith`.  The truth or falsity of the inequality in the base case can be decided by simply doing the necessary arithmetic.  The tactic `decide` can do such calculations, and it proves the base case.

For the induction step, we introduce an arbitrary natural number `n`, assume `n ≥ 5`, and assume the inductive hypothesis, `2 ^ n > n ^ 2`.  Then we use a calculational proof to imitate the reasoning at the end of the *HTPI* proof.  The tactic `linarith` makes inferences that involve combining linear equations and inequalities.  It is able to prove almost all of the inequalities in the calculational proof.  The exception is `n * n ≥ 5 * n` (which is not linear because of the term `n * n`).  So we prove that inequality separately, using a theorem from Lean's library, `Nat.mul_le_mul_right`.  The command `#check @Nat.mul_le_mul_right` tells us the meaning of that theorem:

::: {.ind}
```
@Nat.mul_le_mul_right : ∀ {n m : ℕ} (k : ℕ), n ≤ m → n * k ≤ m * k
```
:::

Thus, `Nat.mul_le_mul_right n` can be used to prove the statement `5 ≤ n → 5 * n ≤ n * n`.  Lean recognizes `x ≥ y` as meaning the same thing as `y ≤ x`, so we can apply this statement to our assumption `n ≥ 5` to prove that `n * n ≥ 5 * n`.  Once we have proven that inequality, the `linarith` tactic can use it to complete the required inequality reasoning.

```lean
theorem Example_6_1_3 : ∀ n ≥ 5, 2 ^ n > n ^ 2 := by
  by_induc
  · -- Base Case
    decide
    done
  · -- Induction Step
    fix n : Nat
    assume h1 : n ≥ 5
    assume ih : 2 ^ n > n ^ 2
    have h2 : n * n ≥ 5 * n := Nat.mul_le_mul_right n h1
    show 2 ^ (n + 1) > (n + 1) ^ 2 from
      calc 2 ^ (n + 1)
        _ = 2 * 2 ^ n := by ring
        _ > 2 * n ^ 2 := by linarith
        _ ≥ n ^ 2 + 5 * n := by linarith
        _ > n ^ 2 + 2 * n + 1 := by linarith
        _ = (n + 1) ^ 2 := by ring
    done
  done
```

Finally, we turn to the question of why we made small changes in two of the examples from *HTPI*.  Perhaps you have guessed by now that we were trying to avoid the use of subtraction.  All of the numbers in the examples in this section were natural numbers, and subtraction of natural numbers is problematic.  In the natural numbers, `3 - 2` is equal to `1`, but what is `2 - 3`?  Lean's answer is `0`.

```lean
++#eval:: 2 - 3     --Answer: 0
```

In Lean, if `a` and `b` are natural numbers and `a < b`, then `a - b` is defined to be `0`.  As a result, the algebraic laws of natural number subtraction are complicated.  For example, `2 - 3 + 1 = 0 + 1 = 1`, but `2 + 1 - 3 = 3 - 3 = 0`, so it is not true that for all natural numbers `a`, `b`, and `c`, `a - b + c = a + c - b`.

If you thought that the answer to the subtraction problem `2 - 3` was `-1`, then you automatically switched from the natural numbers to the integers.  (Recall that the natural numbers are the numbers 0, 1, 2, ..., while the integers are the numbers ..., –3, –2, –1, 0, 1, 2, 3, ....)  To a human mathematician, this is a perfectly natural thing to do: the natural numbers are a subset of the integers, so `2` and `3` are not only natural numbers but also integers, and we can compute `2 - 3` in the integers.

However, that's not how things work in Lean.  In Lean, different types are completely separate.  In particular, `Nat` and `Int` are separate types, and therefore the natural numbers are not a subset of the integers.  Of course, there is an integer 2, but it is different from the natural number 2.  By default, Lean assumes that `2` denotes the natural number 2, but you can specify that you want the integer 2 by writing `(2 : Int)`.  Subtraction of integers in Lean is the subtraction you are familiar with, and it has all the algebraic properties you would expect.  If we want to use subtraction in the theorems in this section, we are better off using familiar integer subtraction rather than funky natural number subtraction.

To prove the theorem in Example 6.1.1 as it appears in *HTPI*, we could state the theorem like this:

```lean
theorem Example_6_1_1 :
    ∀ (n : Nat), Sum i from 0 to n, (2 : Int) ^ i =
    (2 : Int) ^ (n + 1) - (1 : Int)
```

The expression `Sum i from 0 to n, (2 : Int) ^ i` denotes a sum of integers, so it is an integer.  Similarly, the right side of the equation is an integer, and the equation asserts the equality of two integers.  The subtraction on the right side of the equation is integer subtraction, so we can use the usual algebraic laws to reason about it.  In fact, the proof of the theorem in this form is not hard:

```lean
theorem Example_6_1_1 :
    ∀ (n : Nat), Sum i from 0 to n, (2 : Int) ^ i =
    (2 : Int) ^ (n + 1) - (1 : Int) := by
  by_induc
  · -- Base Case
    rewrite [sum_base]
    rfl
    done
  · -- Induction Step
    fix n : Nat
    assume ih : Sum i from 0 to n, (2 : Int) ^ i =
        (2 : Int) ^ (n + 1) - (1 : Int)
    show Sum i from 0 to n + 1, (2 : Int) ^ i =
        (2 : Int) ^ (n + 1 + 1) - (1 : Int) from
      calc Sum i from 0 to n + 1, (2 : Int) ^ i
        _ = (Sum i from 0 to n, (2 : Int) ^ i)
            + (2 : Int) ^ (n + 1) := by rw [sum_from_zero_step]
        _ = (2 : Int) ^ (n + 1) - (1 : Int)
            + (2 : Int) ^ (n + 1) := by rw [ih]
        _ = (2 : Int) ^ (n + 1 + 1) - (1 : Int) := by ring
    done
  done
```

If you change `(2 : Int)` and `(1 : Int)` to `2` and `1`, then the right side of the equation will be a difference of two natural numbers, and Lean will interpret the subtraction as natural number subtraction.  The proof won't work because the `ring` tactic is not able to deal with the peculiar algebraic properties of natural number subtraction.  (The theorem is still true, but the proof is harder.)

### Exercises

::: {.numex arguments="1"}
```lean
theorem Like_Exercise_6_1_1 :
    ∀ (n : Nat), 2 * Sum i from 0 to n, i = n * (n + 1) := sorry
```
:::

::: {.numex arguments="2"}
```lean
theorem Like_Exercise_6_1_4 :
    ∀ (n : Nat), Sum i from 0 to n, 2 * i + 1 = (n + 1) ^ 2 := sorry
```
:::

::: {.numex arguments="3"}
```lean
theorem Exercise_6_1_9a : ∀ (n : Nat), 2 ∣ n ^ 2 + n := sorry
```
:::

::: {.numex arguments="4"}
```lean
theorem Exercise_6_1_13 :
    ∀ (a b : Int) (n : Nat), (a - b) ∣ (a ^ n - b ^ n) := sorry
```
:::

::: {.numex arguments="5"}
```lean
theorem Exercise_6_1_15 : ∀ n ≥ 10, 2 ^ n > n ^ 3 := sorry
```
:::

::: {.numex arguments="6"}
```lean
lemma nonzero_is successor :
    ∀ (n : Nat), n ≠ 0 → ∃ (m : Nat), n = m + 1 := sorry
```
:::

For the next two exercises you will need the following definitions:

```lean
def nat_even (n : Nat) : Prop := ∃ (k : Nat), n = 2 * k

def nat_odd (n : Nat) : Prop := ∃ (k : Nat), n = 2 * k + 1
```

::: {.numex arguments="7"}
```lean
theorem Exercise_6_1_16a1 :
    ∀ (n : Nat), nat_even n ∨ nat_odd n := sorry
```
:::

::: {.numex arguments="8"}
```lean
--Hint:  You may find the lemma nonzero_is_successor
--from a previous exercise useful, as well as Nat.add_right_cancel.
theorem Exercise_6_1_16a2 :
    ∀ (n : Nat), ¬(nat_even n ∧ nat_odd n) := sorry
```
:::

## 6.2. More Examples

We saw in the last section that mathematical induction can be used to prove theorems about calculations involving natural numbers.  But mathematical induction has a much wider range of uses.  Section 6.2 of *HTPI* illustrates this by proving two theorems about finite sets.

How can mathematical induction be used to prove a statement about finite sets?  To say that a set is finite means that it has $n$ elements, for some natural number $n$.  Thus, to say that all finite sets have some property, we can say that for every natural number $n$, every set with $n$ elements has the property.  Since this statement starts with "for every natural number $n$," we can use mathematical induction to try to prove it.

What does it mean to say that a set "has $n$ elements"?  Section 6.2 of *HTPI* says that for the proofs in that section, "an intuitive understanding of this concept will suffice."  Unfortunately, intuition is not Lean's strong suit!  So we'll need to be more explicit about how to talk about finite sets in Lean.

In Chapter 8, we'll define `numElts A n` to be a proposition saying that the set `A` has `n` elements, and we'll prove several theorems involving that proposition.  Those theorems make precise and explicit the intuitive ideas that we'll need in this section.  We'll state those theorems here and use them in our proofs, but you'll have to wait until Section 8.1½ to see how they are proven.  Here are the theorems we'll need:

```lean
theorem zero_elts_iff_empty {U : Type} (A : Set U) :
    numElts A 0 ↔ empty A

theorem one_elt_iff_singleton {U : Type} (A : Set U) :
    numElts A 1 ↔ ∃ (x : U), A = {x}

theorem nonempty_of_pos_numElts {U : Type} {A : Set U} {n : Nat}
    (h1 : numElts A n) (h2 : n > 0) : ∃ (x : U), x ∈ A

theorem remove_one_numElts {U : Type} {A : Set U} {n : Nat} {a : U}
    (h1 : numElts A (n + 1)) (h2 : a ∈ A) : numElts (A \ {a}) n
```

These theorems should make intuitive sense.  The first says that a set has zero elements if and only if it is empty, and the second says that a set has one element if and only if it is a singleton set.  The third theorem says that if a set has a positive number of elements, then there is something in the set.  And the fourth says that if a set has $n + 1$ elements and you remove one element, then the resulting set has $n$ elements.  You can probably guess that we'll be using the last theorem in the induction steps of our proofs.

Our first theorem about finite sets says that if $R$ is a partial order on $A$, then every finite, nonempty subset of $A$ has an $R$-minimal element.  (This is not true in general for infinite subsets of $A$.  Can you think of an example of an infinite subset of a partially ordered set that has no minimal element?)  To say that a set is finite and nonempty we can say that it has $n$ elements for some $n \ge 1$.  So here's how we state our theorem in Lean:

```lean
theorem Example_6_2_1 {A : Type} (R : BinRel A) (h : partial_order R) :
    ∀ n ≥ 1, ∀ (B : Set A), numElts B n →
      ∃ (x : A), minimalElt R x B
```

When we use mathematical induction to prove this theorem, the base case will be `n = 1`.  To write the proof for the base case, we start by assuming `B` is a set with one element.  We can then use the theorem `one_elt_iff_singleton` to conclude that `B = {b}`, for some `b` of type `A`.  We need to prove that `B` has a minimal element, and the only possibility for the minimal element is `b`.  Verifying that `minimalElt R b B` is straightforward.  Here is the proof of the base case:

```lean
theorem Example_6_2_1 {A : Type} (R : BinRel A) (h : partial_order R) :
    ∀ n ≥ 1, ∀ (B : Set A), numElts B n →
      ∃ (x : A), minimalElt R x B := by
  by_induc
  · -- Base Case
    fix B : Set A
    assume h2 : numElts B 1
    rewrite [one_elt_iff_singleton] at h2
    obtain (b : A) (h3 : B = {b}) from h2
    apply Exists.intro b
    define         --Goal : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
    apply And.intro
    · -- Proof that b ∈ B
      rewrite [h3]    --Goal : b ∈ {b}
      define          --Goal : b = b
      rfl
      done
    · -- Proof that nothing in B is smaller than b
      by_contra h4
      obtain (x : A) (h5 : x ∈ B ∧ R x b ∧ x ≠ b) from h4
      have h6 : x ∈ B := h5.left
      rewrite [h3] at h6   --h6 : x ∈ {b}
      define at h6         --h6 : x = b
      show False from h5.right.right h6
      done
    done
  · -- Induction Step

    **done::
  done
```

Notice that since the definition of `minimalElt R b B` involves a negative statement, we found it convenient to use proof by contradiction to prove it.

For the induction step, we assume that `n ≥ 1` and that every set with `n` elements has an `R`-minimal element.  We must prove that every set with `n + 1` elements has a minimal element, so we let `B` be an arbitrary set with `n + 1` elements.  To apply the inductive hypothesis, we need a set with `n` elements.  So we pick some `b ∈ B` (using the theorem `nonempty_of_pos_numElts`) and then remove it from `B` to get the set `B' = B \ {b}`.  The theorem `remove_one_numElts` tells us that `B'` has `n` elements, so by the inductive hypothesis, we can then let `c` be a minimal element of `B'`.  We now know about two elements of `B`:  `b` and `c`.  Which will be a minimal element of `B`?  As explained in *HTPI*, it depends on whether or not `R b c`.  We'll prove that if `R b c`, then `b` is a minimal element of `B`, and if not, then `c` is a minimal element.  It will be convenient to prove these last two facts separately as lemmas.  The first lemma says that in the situation at this point in the proof, if `R b c`, then `b` is an `R`-minimal element of `B`.  Here is the proof.

```lean
lemma Lemma_6_2_1_1 {A : Type} {R : BinRel A} {B : Set A} {b c : A}
    (h1 : partial_order R) (h2 : b ∈ B) (h3 : minimalElt R c (B \ {b}))
    (h4 : R b c) : minimalElt R b B := by
  define at h3
    --h3 : c ∈ B \ {b} ∧ ¬∃ x ∈ B \ {b}, R x c ∧ x ≠ c
  define  --Goal : b ∈ B ∧ ¬∃ x ∈ B, R x b ∧ x ≠ b
  apply And.intro h2    --Goal : ¬∃ x ∈ B, R x b ∧ x ≠ b
  contradict h3.right with h5
  obtain (x : A) (h6 : x ∈ B ∧ R x b ∧ x ≠ b) from h5
  apply Exists.intro x  --Goal : x ∈ B \ {b} ∧ R x c ∧ x ≠ c
  apply And.intro
  · -- Proof that x ∈ B \ {b}
    show x ∈ B \ {b} from And.intro h6.left h6.right.right
    done
  · -- Proof that R x c ∧ x ≠ c
    have Rtrans : transitive R := h1.right.left
    have h7 : R x c := Rtrans x b c h6.right.left h4
    apply And.intro h7
    by_contra h8
    rewrite [h8] at h6  --h6 : c ∈ B ∧ R c b ∧ c ≠ b
    have Rantisymm : antisymmetric R := h1.right.right
    have h9 : c = b := Rantisymm c b h6.right.left h4
    show False from h6.right.right h9
    done
  done
```

The second lemma says that if `¬R b c`, then `c` is an `R`-minimal element of `B`.  We'll leave the proof as an exercise for you:

```lean
lemma Lemma_6_2_1_2 {A : Type} {R : BinRel A} {B : Set A} {b c : A}
    (h1 : partial_order R) (h2 : b ∈ B) (h3 : minimalElt R c (B \ {b}))
    (h4 : ¬R b c) : minimalElt R c B := sorry
```

With this preparation, we are finally ready to give the proof of the induction step of `Example_6_2_1`:

```lean
theorem Example_6_2_1 {A : Type} (R : BinRel A) (h : partial_order R) :
    ∀ n ≥ 1, ∀ (B : Set A), numElts B n →
      ∃ (x : A), minimalElt R x B := by
  by_induc
  · -- Base Case
    ...
  · -- Induction Step
    fix n : Nat
    assume h2 : n ≥ 1
    assume ih : ∀ (B : Set A), numElts B n → ∃ (x : A), minimalElt R x B
    fix B : Set A
    assume h3 : numElts B (n + 1)
    have h4 : n + 1 > 0 := by linarith
    obtain (b : A) (h5 : b ∈ B) from nonempty_of_pos_numElts h3 h4
    set B' : Set A := B \ {b}
    have h6 : numElts B' n := remove_one_numElts h3 h5
    obtain (c : A) (h7 : minimalElt R c B') from ih B' h6
    by_cases h8 : R b c
    · -- Case 1. h8 : R b c
      have h9 : minimalElt R b B := Lemma_6_2_1_1 h h5 h7 h8
      show ∃ (x : A), minimalElt R x B from Exists.intro b h9
      done
    · -- Case 2. h8 : ¬R b c
      have h9 : minimalElt R c B := Lemma_6_2_1_2 h h5 h7 h8
      show ∃ (x : A), minimalElt R x B from Exists.intro c h9
      done
    done
  done
```

We'll consider one more theorem from Section 6.2 of *HTPI*.  Example 6.2.2 proves that a partial order on a finite set can always be extended to a total order.  Rather than give that proof, we are going to prove the more general theorem that is stated in Exercise 2 in Section 6.2 of *HTPI*.  To explain the theorem in that exercise, it will be helpful to introduce a bit of terminology.  Suppose `R` is a partial order on `A` and `b` has type `A`.  We will say that `b` is *`R`-comparable to everything* if `∀ (x : A), R b x ∨ R x b`.  If `B` is a set of objects of type `A`, we say that `B` is *`R`-comparable to everything* if every element of `B` is `R`-comparable to everything; that is, if `∀ b ∈ B, ∀ (x : A), R b x ∨ R x b`.  Finally, we say that another binary relation `T` *extends* `R` if `∀ (x y : A), R x y → T x y`.  We are going to prove that if `R` is a partial order on `A` and `B` is a finite set of objects of type `A`, then there is a partial order `T` that extends `R` such that `B` is `T`-comparable to everything.  In other words, we are going to prove the following theorem:

```lean
theorem Exercise_6_2_2 {A : Type} (R : BinRel A) (h : partial_order R) :
    ∀ (n : Nat) (B : Set A), numElts B n → ∃ (T : BinRel A),
    partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧
    ∀ x ∈ B, ∀ (y : A), T x y ∨ T y x
```

In the exercises, we will ask you to show that this implies the theorem in Example 6.2.2.

It will be helpful to begin with a warm-up exercise.  We'll show that a partial order can always be extended to make a single object comparable to everything.  In other words, we'll show that if `R` is a partial order on `A` and `b` has type `A`, then we can define a partial order `T` extending `R` such that `b` is `T`-comparable to everything.  To define `T`, we will need to make sure that for every `x` of type `A`, either `T b x` or `T x b`.  If `R x b`, then since `T` must extend `R`, we must have `T x b`.  If `¬R x b`, then we will define `T` so that `T b x`.  But notice that if we follow this plan, then for any `x` and `y`, if we have `R x b` and `¬R y b`, then we will have `T x b` and `T b y`, and since `T` must be transitive, we must then have `T x y`.  Summing up, if we have `R x y` then we must have `T x y`, and if we have `R x b` and `¬R y b` then we will also need to have `T x y`.  So let's try defining `T x y` to mean `R x y ∨ (R x b ∧ ¬R y b)`.

It will be useful to have a name for this relation `T`.  Since it is an extension of `R` determined by the element `b`, we will give it the name `extendPO R b`.  Here is the definition of this relation:

```lean
def extendPO {A : Type} (R : BinRel A) (b : A) (x y : A) : Prop :=
  R x y ∨ (R x b ∧ ¬R y b)
```

We need to prove a number of things about `extendPO R b`.  First of all, we need to prove that it is a partial order.  We'll leave most of the details as exercises for you:

```lean
lemma extendPO_is_ref {A : Type} (R : BinRel A) (b : A)
    (h : partial_order R) : reflexive (extendPO R b) := sorry

lemma extendPO_is_trans {A : Type} (R : BinRel A) (b : A)
    (h : partial_order R) : transitive (extendPO R b) := sorry

lemma extendPO_is_antisymm {A : Type} (R : BinRel A) (b : A)
    (h : partial_order R) : antisymmetric (extendPO R b) := sorry

lemma extendPO_is_po {A : Type} (R : BinRel A) (b : A)
    (h : partial_order R) : partial_order (extendPO R b) := 
  And.intro (extendPO_is_ref R b h)
    (And.intro (extendPO_is_trans R b h) (extendPO_is_antisymm R b h))
```

It is easy to prove that `extendPO R b` extends `R`:

```lean
lemma extendPO_extends {A : Type} (R : BinRel A) (b : A) (x y : A) :
    R x y → extendPO R b x y := by
  assume h1 : R x y
  define
  show R x y ∨ R x b ∧ ¬R y b from Or.inl h1
  done
```

Finally, we verify that `extendPO R b` does what it was supposed to do: it makes `b` comparable with everything:

```lean
lemma extendPO_all_comp {A : Type} (R : BinRel A) (b : A)
    (h : partial_order R) :
    ∀ (x : A), extendPO R b b x ∨ extendPO R b x b := by
  have Rref : reflexive R := h.left
  fix x : A
  or_left with h1
  define at h1     --h1 : ¬(R x b ∨ R x b ∧ ¬R b b)
  demorgan at h1   --h1 : ¬R x b ∧ ¬(R x b ∧ ¬R b b)
  define           --Goal : R b x ∨ R b b ∧ ¬R x b
  apply Or.inr
  show R b b ∧ ¬R x b from And.intro (Rref b) h1.left
  done
```

With this preparation, we can finally return to our theorem `Exercise_6_2_2`.  We will prove it by mathematical induction.  In the base case we must show that if `B` has 0 elements then we can extend `R` to make everything in `B` comparable to everything.  Of course, no extension is necessary, since it is vacuously true that all elements of `B` are `R`-comparable to everything.  For the induction step, after assuming the inductive hypothesis, we must prove that if `B` has `n + 1` elements then we can extend `R` to make all elements of `B` comparable to everything.  As before, we choose `b ∈ B` and let `B' = B \ {b}`.  By inductive hypothesis, we can find an extension `T'` of `R` that makes all elements of `B'` comparable to everything, so we just have to extend `T'` further to make `b` comparable to everything.  But as we have just seen, we can do this with `extendPO T' b`.

```lean
theorem Exercise_6_2_2 {A : Type} (R : BinRel A) (h : partial_order R) :
    ∀ (n : Nat) (B : Set A), numElts B n → ∃ (T : BinRel A),
    partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧
    ∀ x ∈ B, ∀ (y : A), T x y ∨ T y x := by
  by_induc
  · -- Base Case
    fix B : Set A
    assume h2 : numElts B 0
    rewrite [zero_elts_iff_empty] at h2
    define at h2     --h2 : ¬∃ (x : A), x ∈ B
    apply Exists.intro R
    apply And.intro h
    apply And.intro
    · -- Proof that R extends R
      fix x : A; fix y : A
      assume h3 : R x y
      show R x y from h3
      done
    · -- Proof that everything in B comparable to everything under R
      fix x : A
      assume h3 : x ∈ B
      contradict h2
      show ∃ (x : A), x ∈ B from Exists.intro x h3
      done
    done
  · -- Induction Step
    fix n : Nat
    assume ih : ∀ (B : Set A), numElts B n → ∃ (T : BinRel A),
      partial_order T ∧ (∀ (x y : A), R x y → T x y) ∧
      ∀ (x : A), x ∈ B → ∀ (y : A), T x y ∨ T y x
    fix B : Set A
    assume h2 : numElts B (n + 1)
    have h3 : n + 1 > 0 := by linarith
    obtain (b : A) (h4 : b ∈ B) from nonempty_of_pos_numElts h2 h3
    set B' : Set A := B \ {b}
    have h5 : numElts B' n := remove_one_numElts h2 h4
    have h6 : ∃ (T : BinRel A), partial_order T ∧
      (∀ (x y : A), R x y → T x y) ∧
      ∀ (x : A), x ∈ B' → ∀ (y : A), T x y ∨ T y x := ih B' h5
    obtain (T' : BinRel A)
      (h7 : partial_order T' ∧ (∀ (x y : A), R x y → T' x y) ∧
      ∀ (x : A), x ∈ B' → ∀ (y : A), T' x y ∨ T' y x) from h6
    have T'po : partial_order T' := h7.left
    have T'extR : ∀ (x y : A), R x y → T' x y := h7.right.left
    have T'compB' : ∀ (x : A), x ∈ B' →
      ∀ (y : A), T' x y ∨ T' y x := h7.right.right
    set T : BinRel A := extendPO T' b
    apply Exists.intro T
    apply And.intro (extendPO_is_po T' b T'po)
    apply And.intro
    · -- Proof that T extends R
      fix x : A; fix y : A
      assume h8 : R x y
      have h9 : T' x y := T'extR x y h8
      show T x y from (extendPO_extends T' b x y h9)
      done
    · -- Proof that everything in B comparable to everything under T
      fix x : A
      assume h8 : x ∈ B
      by_cases h9 : x = b
      · -- Case 1. h9 : x = b
        rewrite [h9]
        show ∀ (y : A), T b y ∨ T y b from extendPO_all_comp T' b T'po
        done
      · -- Case 2. h9 : x ≠ b
        have h10 : x ∈ B' := And.intro h8 h9
        fix y : A
        have h11 : T' x y ∨ T' y x := T'compB' x h10 y
        by_cases on h11
        · -- Case 2.1. h11 : T' x y
          show T x y ∨ T y x from
            Or.inl (extendPO_extends T' b x y h11)
          done
        · -- Case 2.2. h11 : T' y x
          show T x y ∨ T y x from
            Or.inr (extendPO_extends T' b y x h11)
          done
        done
      done
    done
  done
```

### Exercises

::: {.numex arguments="1"}
```lean
lemma Lemma_6_2_1_2 {A : Type} {R : BinRel A} {B : Set A} {b c : A}
    (h1 : partial_order R) (h2 : b ∈ B) (h3 : minimalElt R c (B \ {b}))
    (h4 : ¬R b c) : minimalElt R c B := sorry
```
:::

::: {.numex arguments="2"}
```lean
lemma extendPO_is_ref {A : Type} (R : BinRel A) (b : A)
    (h : partial_order R) : reflexive (extendPO R b) := sorry
```
:::

::: {.numex arguments="3"}
```lean
lemma extendPO_is_trans {A : Type} (R : BinRel A) (b : A)
    (h : partial_order R) : transitive (extendPO R b) := sorry
```
:::

::: {.numex arguments="4"}
```lean
lemma extendPO_is_antisymm {A : Type} (R : BinRel A) (b : A)
    (h : partial_order R) : antisymmetric (extendPO R b) := sorry
```
:::

::: {.numex arguments="5"}
```lean
theorem Exercise_6_2_3 (A : Type) (R : BinRel A)
    (h : total_order R) : ∀ n ≥ 1, ∀ (B : Set A),
    numElts B n → ∃ (b : A), smallestElt R b B := sorry
```
:::

::: {.numex arguments="6"}
```lean
--Hint:  First prove that R is reflexive.
theorem Exercise_6_2_4a {A : Type} (R : BinRel A)
    (h : ∀ (x y : A), R x y ∨ R y x) : ∀ n ≥ 1, ∀ (B : Set A),
    numElts B n → ∃ x ∈ B, ∀ y ∈ B, ∃ (z : A), R x z ∧ R z y := sorry
```
:::

::: {.numex arguments="7"}
```lean
theorem Like_Exercise_6_2_16 {A : Type} (f : A → A)
    (h : one_to_one f) : ∀ (n : Nat) (B : Set A), numElts B n →
    closed f B → ∀ y ∈ B, ∃ x ∈ B, f x = y := sorry
```
:::

::: {.numex arguments="8"}
```lean
--Hint:  Use Exercise_6_2_2.
theorem Example_6_2_2 {A : Type} (R : BinRel A)
    (h1 : ∃ (n : Nat), numElts {x : A | x = x} n)
    (h2 : partial_order R) : ∃ (T : BinRel A),
      total_order T ∧ ∀ (x y : A), R x y → T x y := sorry
```
:::

## 6.3. Recursion

In the last two sections, we saw that we can prove that all natural numbers have some property by proving that 0 has the property, and also that for every natural number $n$, if $n$ has the property then so does $n + 1$.  In this section we will see that a similar idea can be used to define a function whose domain is the natural numbers.  We can define a function $f$ with domain $\mathbb{N}$ by specifying the value of $f(0)$, and also saying how to compute $f(n+1)$ if you already know the value of $f(n)$.

For example, we can define a function $f : \mathbb{N} \to \mathbb{N}$ as follows:

::: {.quote}
$f(0) = 1$;<br>\newline
for every $n \in \mathbb{N}$, $f(n+1) = (n+1) \cdot f(n)$.
:::

Here is the same definition written in Lean.  (For reasons that will become clear shortly, we have given the function the name `fact`.)

```lean
def fact (k : Nat) : Nat :=
  match k with
    | 0 => 1
    | n + 1 => (n + 1) * fact n
```

Lean can use this definition to compute `fact k` for any natural number `k`.  The `match` statement tells Lean to try to match the input `k` with one of the two patterns `0` and `n + 1`, and then to use the corresponding formula after `=>` to compute `fact k`.  For example, if we ask Lean for `fact 4`, it first checks if `4` matches `0`.  Since it doesn't, it goes on to the next line and determines that `4` matches the pattern `n + 1`, with `n = 3`, so it uses the formula `fact 4 = 4 * fact 3`.  Of course, now it must compute `fact 3`, which it does in the same way: `3` matches `n + 1` with `n = 2`, so `fact 3 = 3 * fact 2`.  Continuing in this way, Lean determines that

::: {.ind}
```
fact 4 = 4 * fact 3 = 4 * (3 * fact 2) = 4 * (3 * (2 * fact 1))
       = 4 * (3 * (2 * (1 * fact 0))) = 4 * (3 * (2 * (1 * 1))) = 24.
```
:::

You can confirm this with the `#eval` command:

```lean
#eval fact 4   --Answer: 24
```

Of course, by now you have probably guessed why we used the name `fact` for his function: `fact k` is `k` factorial---the product of all the numbers from 1 to `k`.

This style of definition is called a *recursive* definition.  If a function is defined by a recursive definition, then theorems about that function are often most easily proven by induction.  For example, here is a theorem about the factorial function.  It is Example 6.3.1 in *HTPI*, and we begin the Lean proof by imitating the proof in *HTPI*.

```lean
theorem ??Example_6_3_1:: : ∀ n ≥ 4, fact n > 2 ^ n := by
  by_induc
  · -- Base Case
    decide
    done
  · -- Induction Step
    fix n : Nat
    assume h1 : n ≥ 4
    assume ih : fact n > 2 ^ n
    show fact (n + 1) > 2 ^ (n + 1) from
      calc fact (n + 1)
        _ = (n + 1) * fact n := by rfl
        _ > (n + 1) * 2 ^ n := sorry
        _ > 2 * 2 ^ n := sorry
        _ = 2 ^ (n + 1) := by ring
    done
  done
```

There are two steps in the calculational proof at the end that require justification.  The first says that `(n + 1) * fact n > (n + 1) * 2 ^ n`, which should follow from the inductive hypothesis `ih : fact n > 2 ^ n` by multiplying both sides by `n + 1`.  Is there a theorem that would justify this inference?

This may remind you of a step in `Example_6_1_3` where we used the theorem `Nat.mul_le_mul_right`, which says `∀ {n m : ℕ} (k : ℕ), n ≤ m → n * k ≤ m * k`.  Our situation in this example is similar, but it involves a strict inequality (`>` rather than `≥`) and it involves multiplying on the left rather than the right.  Many theorems about inequalities in Lean's library contain either `le` (for "less than or equal to") or `lt` (for "less than") in their names, but they can also be used to prove statements involving `≥` or `>`.  Perhaps the theorem we need is named something like `Nat.mul_lt_mul_left`.  If you type `#check @Nat.mul_lt_mul_` into VS Code, a pop-up window will appear listing several theorems that begin with `Nat.mul_lt_mul_`.  There is no `Nat.mul_lt_mul_left`, but there is a theorem called `Nat.mul_lt_mul_of_pos_left`, and its meaning is

::: {.ind}
```
@Nat.mul_lt_mul_of_pos_left : ∀ {n m k : ℕ},
                                n < m → k > 0 → k * n < k * m
```
:::

Lean has correctly reminded us that, to multiply both sides of a strict inequality by a number `k`, we need to know that `k > 0`.  So in our case, we'll need to prove that `n + 1 > 0`.  Once we have that, we can use the theorem `Nat.mul_lt_mul_of_pos_left` to eliminate the first `sorry`.

The second `sorry` is similar: `(n + 1) * 2 ^ n > 2 * 2 ^ n` should follow from `n + 1 > 2` and `2 ^ n > 0`, and you can verify that the theorem that will justify this inference is `Nat.mul_lt_mul_of_pos_right`.

So we have three inequalities that we need to prove before we can justify the steps of the calculational proof:  `n + 1 > 0`, `n + 1 > 2`, and `2 ^ n > 0`.  We'll insert `have` steps before the calculational proof to assert these three inequalities.  If you try it, you'll find that `linarith` can prove the first two, but not the third.

How can we prove `2 ^ n > 0`?  It is often helpful to think about whether there is a general principle that is behind a statement we are trying to prove.  In our case, the inequality `2 ^ n > 0` is an instance of the general fact that if `m` and `n` are any natural numbers with `m > 0`, then `m ^ n > 0`.  Maybe that fact is in Lean's library:

```lean
example (m n : Nat) (h : m > 0) : m ^ n > 0 := by ++apply?::
```

The `apply?` tactic comes up with `exact Nat.pos_pow_of_pos n h`, and `#check @Nat.pos_pow_of_pos` gives the result

::: {.ind}
```
@Nat.pos_pow_of_pos : ∀ {n : ℕ} (m : ℕ), 0 < n → 0 < n ^ m
```
:::

That means that we can use `Nat.pos_pow_of_pos` to prove `2 ^ n > 0`, but first we'll need to prove that `2 > 0`.  We now have all the pieces we need; putting them together leads to this proof:

```lean
theorem Example_6_3_1 : ∀ n ≥ 4, fact n > 2 ^ n := by
  by_induc
  · -- Base Case
    decide
    done
  · -- Induction Step
    fix n : Nat
    assume h1 : n ≥ 4
    assume ih : fact n > 2 ^ n
    have h2 : n + 1 > 0 := by linarith
    have h3 : n + 1 > 2 := by linarith
    have h4 : 2 > 0 := by linarith
    have h5 : 2 ^ n > 0 := Nat.pos_pow_of_pos n h4
    show fact (n + 1) > 2 ^ (n + 1) from
      calc fact (n + 1)
        _ = (n + 1) * fact n := by rfl
        _ > (n + 1) * 2 ^ n := Nat.mul_lt_mul_of_pos_left ih h2
        _ > 2 * 2 ^ n := Nat.mul_lt_mul_of_pos_right h3 h5
        _ = 2 ^ (n + 1) := by ring
    done
  done
```

But there is an easier way.  Look at the two ">" steps in the calculational proof at the end of `Example_6_3_1`.  In both cases, we took a known relationship between two quantities and did something to both sides that preserved the relationship.  In the first case, the known relationship was `ih : fact n > 2 ^ n`, and we multiplied both sides by `n + 1` on the left; in the second, the known relationship was `h3 : n + 1 > 2`, and we multiplied both sides by `2 ^ n` on the right.  To justify these steps, we had to find the right theorems in Lean's library, and we ended up needing auxiliary positivity facts: `h2 : n + 1 > 0` in the first case and `h5 : 2 ^ n > 0` in the second.  There is a tactic that can simplify these steps: if `h` is a proof of a statement asserting a relationship between two quantities, then the tactic `rel [h]` will attempt to prove any statement obtained from that relationship by applying the same operation to both sides.  The tactic will try to find a theorem in Lean's library that says that the operation preserves the relationship, and if the theorem requires auxiliary positivity facts, it will try to prove those facts as well.  The `rel` tactic doesn't always succeed, but when it does, it saves you the trouble of searching through the library for the necessary theorems.  In this case, the tactic allows us to give a much simpler proof of `Example_6_3_1`:

```lean
theorem Example_6_3_1 : ∀ n ≥ 4, fact n > 2 ^ n := by
  by_induc
  · -- Base Case
    decide
    done
  · -- Induction Step
    fix n : Nat
    assume h1 : n ≥ 4
    assume ih : fact n > 2 ^ n
    have h2 : n + 1 > 2 := by linarith
    show fact (n + 1) > 2 ^ (n + 1) from
      calc fact (n + 1)
        _ = (n + 1) * fact n := by rfl
        _ > (n + 1) * 2 ^ n := by rel [ih]
        _ > 2 * 2 ^ n := by rel [h2]
        _ = 2 ^ (n + 1) := by ring
    done
  done
```

The next example in *HTPI* is a proof of one of the laws of exponents:  `a ^ (m + n) = a ^ m * a ^ n`.  Lean's definition of exponentiation with natural number exponents is recursive.  The definitions Lean uses are essentially as follows:

```lean
--For natural numbers b and k, b ^ k = nat_pow b k:
def nat_pow (b k : Nat) : Nat :=
  match k with
    | 0 => 1
    | n + 1 => (nat_pow b n) * b

--For a real number b and a natural number k, b ^ k = real_pow b k:
def real_pow (b : Real) (k : Nat) : Real :=
  match k with
    | 0 => 1
    | n + 1 => (real_pow b n) * b
```

Let's prove the addition law for exponents:

```lean
theorem Example_6_3_2_cheating : ∀ (a : Real) (m n : Nat),
    a ^ (m + n) = a ^ m * a ^ n := by
  fix a : Real; fix m : Nat; fix n : Nat
  ring
  done
```

Well, that wasn't really fair.  The `ring` tactic knows the laws of exponents, so it has no trouble proving this theorem.  But we want to know *why* the law holds, so let's see if we can prove it without using `ring`.  The following proof is essentially the same as the proof in *HTPI*:

```lean
theorem Example_6_3_2 : ∀ (a : Real) (m n : Nat),
    a ^ (m + n) = a ^ m * a ^ n := by
  fix a : Real; fix m : Nat
    --Goal : ∀ (n : Nat), a ^ (m + n) = a ^ m * a ^ n
  by_induc
  · -- Base Case
    show a ^ (m + 0) = a ^ m * a ^ 0 from
      calc a ^ (m + 0)
        _ = a ^ m := by rfl
        _ = a ^ m * 1 := (mul_one (a ^ m)).symm
        _ = a ^ m * a ^ 0 := by rfl
    done
  · -- Induction Step
    fix n : Nat
    assume ih : a ^ (m + n) = a ^ m * a ^ n
    show a ^ (m + (n + 1)) = a ^ m * a ^ (n + 1) from
      calc a ^ (m + (n + 1))
        _ = a ^ ((m + n) + 1) := by rw [add_assoc]
        _ = a ^ (m + n) * a := by rfl
        _ = (a ^ m * a ^ n) * a := by rw [ih]
        _ = a ^ m * (a ^ n * a) := by rw [mul_assoc]
        _ = a ^ m * (a ^ (n + 1)) := by rfl
    done
  done
```

Finally, we'll prove the theorem in Example 6.3.4 of *HTPI*, which again involves exponentiation with natural number exponents.  Here's the beginning of the proof:

::: {.inout}
::: {.inpt}
```lean
theorem Example_6_3_4 : ∀ (x : Real), x > -1 →
    ∀ (n : Nat), (1 + x) ^ n ≥ 1 + n * x := by
  fix x : Real
  assume h1 : x > -1
  **done::
```
:::

::: {.outpt}
```state
x : ℝ
h1 : x > -1
⊢ ∀ (n : ℕ),
>>  (1 + x) ^ n ≥
>>    1 + ↑n * x
```
:::
:::

Look carefully at the goal in the tactic state.  Why is there a `↑` before the last `n`?  The reason has to do with types.  The variable `x` has type `Real` and `n` has type `Nat`, so how can Lean multiply `n` by `x`?  Remember, in Lean, the natural numbers are not a subset of the real numbers.  The two types are completely separate, but for each natural number, there is a corresponding real number.  To multiply `n` by `x`, Lean had to convert `n` to the corresponding real number, through a process called *coercion*.  The notation `↑n` denotes the result of *coercing* (or *casting*) `n` to another type---in this case, `Real`.  Since `↑n` and `x` are both real numbers, Lean can use the multiplication operation on the real numbers to multiply them.  (To type `↑` in VSCode, type `\uparrow`, or just `\u`.)

As we will see, the need for coercion in this example will make the proof a bit more complicated, because we'll need to use some theorems about coercions.  Theorems about coercion of natural numbers to some other type often have names that start `Nat.cast`.

Continuing with the proof, since exponentiation is defined recursively, let's try mathematical induction:

::: {.inout}
::: {.inpt}
```lean
theorem Example_6_3_4 : ∀ (x : Real), x > -1 →
    ∀ (n : Nat), (1 + x) ^ n ≥ 1 + n * x := by
  fix x : Real
  assume h1 : x > -1
  by_induc
  · -- Base Case

    **done::
  · -- Induction Step

    **done::  
  done
```
:::

::: {.outpt}
```state
case Base_Case
x : ℝ
h1 : x > -1
⊢ (1 + x) ^ 0 ≥
>>  1 + ↑0 * x
```
:::
:::

You might think that `linarith` could prove the goal for the base case, but it can't.  The problem is the `↑0`, which denotes the result of coercing the natural number `0` to a real number.  Of course, that should be the real number `0`, but is it?  Yes, but the `linarith` tactic doesn't know that.  The theorem `Nat.cast_zero` says that `↑0 = 0` (where the `0` on the right side of the equation is the *real number* `0`), so the tactic `rewrite [Nat.cast_zero]` will convert `↑0` to `0`.  After that step, `linarith` can complete the proof of the base case, and we can start on the induction step.

::: {.inout}
::: {.inpt}
```lean
theorem Example_6_3_4 : ∀ (x : Real), x > -1 →
    ∀ (n : Nat), (1 + x) ^ n ≥ 1 + n * x := by
  fix x : Real
  assume h1 : x > -1
  by_induc
  · -- Base Case
    rewrite [Nat.cast_zero]
    linarith
    done
  · -- Induction Step
    fix n : Nat
    assume ih : (1 + x) ^ n ≥ 1 + n * x
    **done::
  done
```
:::

::: {.outpt}
```state
case Induction_Step
x : ℝ
h1 : x > -1
n : ℕ
ih : (1 + x) ^ n ≥
>>    1 + ↑n * x
⊢ (1 + x) ^ (n + 1) ≥
>>  1 + ↑(n + 1) * x
```
:::
:::

Once again, there's a complication caused by coercion.  The inductive hypothesis talks about `↑n`, but the goal involves `↑(n + 1)`.  What is the relationship between these?  Surely it should be the case that `↑(n + 1) = ↑n + 1`; that is, the result of coercing the natural number `n + 1` to a real number should be one larger than the result of coercing `n` to a real number.  The theorem `Nat.cast_succ` says exactly that, so `rewrite [Nat.cast_succ]` will change the `↑(n + 1)` in the goal to `↑n + 1`.  (The number `n + 1` is sometimes called the *successor* of `n`, and `succ` is short for "successor.")  With that change, we can continue with the proof.  The following proof is modeled on the proof in *HTPI*.

```lean
theorem ??Example_6_3_4:: : ∀ (x : Real), x > -1 →
    ∀ (n : Nat), (1 + x) ^ n ≥ 1 + n * x := by
  fix x : Real
  assume h1 : x > -1
  by_induc
  · -- Base Case
    rewrite [Nat.cast_zero]
    linarith
    done
  · -- Induction Step
    fix n : Nat
    assume ih : (1 + x) ^ n ≥ 1 + n * x
    rewrite [Nat.cast_succ]
    show (1 + x) ^ (n + 1) ≥ 1 + (n + 1) * x from
      calc (1 + x) ^ (n + 1)
        _ = (1 + x) ^ n * (1 + x) := by rfl
        _ ≥ (1 + n * x) * (1 + x) := sorry
        _ = 1 + n * x + x + n * x ^ 2 := by ring
        _ ≥ 1 + n * x + x + 0 := sorry
        _ = 1 + (n + 1) * x := by ring
    done
  done
```

Note that in the calculational proof, each `n` or `n + 1` that is multiplied by `x` is really `↑n` or `↑n + 1`, but we don't need to say so explicitly; Lean fills in coercions automatically when they are required.

All that's left is to replace the two occurrences of `sorry` with justifications.  The first `sorry` step should follow from the inductive hypothesis by multiplying both sides by `1 + x`, so a natural attempt to justify it would be `by rel [ih]`.  Unfortunately, we get an error message saying that `rel` failed.  The error message tells us that `rel` needed to know that `0 ≤ 1 + x`, and it was unable to prove it, so we'll have to provide a proof of that statement ourselves.  Fortunately, `linarith` can handle it (deducing it from `h1 : x > -1`), and once we fill in that additional step, the `rel` tactic succeeds.

```lean
theorem ??Example_6_3_4:: : ∀ (x : Real), x > -1 →
    ∀ (n : Nat), (1 + x) ^ n ≥ 1 + n * x := by
  fix x : Real
  assume h1 : x > -1
  by_induc
  · -- Base Case
    rewrite [Nat.cast_zero]
    linarith
    done
  · -- Induction Step
    fix n : Nat
    assume ih : (1 + x) ^ n ≥ 1 + n * x
    rewrite [Nat.cast_succ]
    have h2 : 0 ≤ 1 + x := by linarith
    show (1 + x) ^ (n + 1) ≥ 1 + (n + 1) * x from
      calc (1 + x) ^ (n + 1)
        _ = (1 + x) ^ n * (1 + x) := by rfl
        _ ≥ (1 + n * x) * (1 + x) := by rel [ih]
        _ = 1 + n * x + x + n * x ^ 2 := by ring
        _ ≥ 1 + n * x + x + 0 := sorry
        _ = 1 + (n + 1) * x := by ring
    done
  done
```

For the second `sorry` step, we'll need to know that `n * x ^ 2 ≥ 0`.  To prove it, we start with the fact that the square of any real number is nonnegative:

::: {.ind}
```
@sq_nonneg : ∀ {α : Type u_1} [inst : LinearOrderedSemiring α]
              [inst_1 : ExistsAddOfLE α]
              (a : α), 0 ≤ a ^ 2
```
:::

As usual, we don't need to pay much attention to the implicit arguments; what is important is the last line, which tells us that `sq_nonneg x` is a proof of `x ^ 2 ≥ 0`.  To get `n * x ^ 2 ≥ 0` we just have to multiply both sides by `n`, which we can justify with the `rel` tactic, and then one more application of `rel` will handle the remaining `sorry`.  Here is the complete proof:

```lean
theorem Example_6_3_4 : ∀ (x : Real), x > -1 →
    ∀ (n : Nat), (1 + x) ^ n ≥ 1 + n * x := by
  fix x : Real
  assume h1 : x > -1
  by_induc
  · -- Base Case
    rewrite [Nat.cast_zero]
    linarith
    done
  · -- Induction Step
    fix n : Nat
    assume ih : (1 + x) ^ n ≥ 1 + n * x
    rewrite [Nat.cast_succ]
    have h2 : 0 ≤ 1 + x := by linarith
    have h3 : x ^ 2 ≥ 0 := sq_nonneg x
    have h4 : n * x ^ 2 ≥ 0 :=
      calc n * x ^ 2
        _ ≥ n * 0 := by rel [h3]
        _ = 0 := by ring
    show (1 + x) ^ (n + 1) ≥ 1 + (n + 1) * x from
      calc (1 + x) ^ (n + 1)
        _ = (1 + x) ^ n * (1 + x) := by rfl
        _ ≥ (1 + n * x) * (1 + x) := by rel [ih]
        _ = 1 + n * x + x + n * x ^ 2 := by ring
        _ ≥ 1 + n * x + x + 0 := by rel [h4]
        _ = 1 + (n + 1) * x := by ring
    done
  done
```

Before ending this section, we'll return to a topic left unexplained before.  We can now describe how `Sum i from k to n, f i` is defined.  The key is a function `sum_seq`, which is defined by recursion:

```lean
def sum_seq {A : Type} [AddZeroClass A]
    (m k : Nat) (f : Nat → A) : A :=
  match m with
    | 0 => 0
    | n + 1 => sum_seq n k f + f (k + n)
```

To get an idea of what this definition means, let's try evaluating `sum_seq 3 k f`:

::: {.ind}
```
sum_seq 3 k f = sum_seq 2 k f + f (k + 2)
              = sum_seq 1 k f + f (k + 1) + f (k + 2)
              = sum_seq 0 k f + f (k + 0) + f (k + 1) + f (k + 2)
              = 0 + f (k + 0) + f (k + 1) + f (k + 2)
              = f k + f (k + 1) + f (k + 2).
```
:::

So `sum_seq 3 k f` adds up three consecutive values of `f`, starting with `f k`.  More generally, `sum_seq n k f` adds up a sequence of `n` consecutive values of `f`, starting with `f k`.  (The implicit arguments say that the type of the values of `f` can be any type for which `+` and `0` make sense.)  The notation `Sum i from k to n, f i` is now defined to be a shorthand for `sum_seq (n + 1 - k) k f`.  We'll leave it to you to puzzle out why that gives the desired result.

### Exercises

::: {.numex arguments="1"}
```lean
theorem Exercise_6_3_4 : ∀ (n : Nat),
    3 * (Sum i from 0 to n, (2 * i + 1) ^ 2) =
    (n + 1) * (2 * n + 1) * (2 * n + 3) := sorry
```
:::

::: {.numex arguments="2"}
```lean
theorem Exercise_6_3_7b (f : Nat → Real) (c : Real) : ∀ (n : Nat),
    Sum i from 0 to n, c * f i = c * Sum i from 0 to n, f i := sorry
```
:::

::: {.numex arguments="3"}
```lean
theorem fact_pos : ∀ (n : Nat), fact n ≥ 1 := sorry
```
:::

::: {.numex arguments="4"}
```lean
--Hint:  Use the theorem fact_pos from the previous exercise.
theorem Exercise_6_3_13a (k : Nat) : ∀ (n : Nat),
    fact (k ^ 2 + n) ≥ k ^ (2 * n) := sorry
```
:::

::: {.numex arguments="5"}
```lean
--Hint:  Use the theorem in the previous exercise.
--You may find it useful to first prove a lemma:
--∀ (k : Nat), 2 * k ^ 2 + 1 ≥ k
theorem Exercise_6_3_13b (k : Nat) : ∀ n ≥ 2 * k ^ 2,
    fact n ≥ k ^ n := sorry
```
:::

6\. A sequence is defined recursively as follows:

```lean
def seq_6_3_15 (k : Nat) : Int :=
  match k with
    | 0 => 0
    | n + 1 => 2 * seq_6_3_15 n + n
```

Prove the following theorem about this sequence:

```lean
theorem Exercise_6_3_15 : ∀ (n : Nat),
    seq_6_3_15 n = 2 ^ n - n - 1 := sorry
```

7\. A sequence is defined recursively as follows:

```lean
def seq_6_3_16 (k : Nat) : Nat :=
  match k with
    | 0 => 2
    | n + 1 => (seq_6_3_16 n) ^ 2
```

Find a formula for `seq_6_3_16 n`.  Fill in the blank in the theorem below with your formula and then prove the theorem.

```lean
theorem Exercise_6_3_16 : ∀ (n : Nat),
    seq_6_3_16 n = ___ := sorry
```

## 6.4. Strong Induction

In the induction step of a proof by mathematical induction, we prove that a natural number has some property from the assumption that the previous number has the property.  Section 6.4 of *HTPI* introduces a version of mathematical induction in which we get to assume that *all* smaller numbers have the property.  Since this is a stronger assumption, this version of induction is called *strong induction*.  Here is how strong induction works (*HTPI* p. 304):

#### To prove a goal of the form `∀ (n : Nat), P n`:

::: {.ind}
Prove that `∀ (n : Nat), (∀ n_1 < n, P n_1) → P n`.
:::

To write a proof by strong induction in Lean, we use the tactic `by_strong_induc`, whose effect on the tactic state can be illustrated as follows.

::: {.lftrt}
::: {.bef}
```state
>> ⋮
⊢ ∀ (n : Nat), P n
```
:::

::: {.aft}
```state
>> ⋮
⊢  ∀ (n : Nat),
>>  (∀ n_1 < n, P n_1) → P n
```
:::
:::

To illustrate this, we begin with Example 6.4.1 of *HTPI*.

```lean
theorem Example_6_4_1 : ∀ m > 0, ∀ (n : Nat),
    ∃ (q r : Nat), n = m * q + r ∧ r < m
```

Imitating the strategy of the proof in *HTPI*, we let `m` be an arbitrary natural number, assume `m > 0`, and then prove the statement `∀ (n : Nat), ∃ (q r : Nat), n = m * q + r ∧ r < m` by strong induction.  That means that after introducing an arbitrary natural number `n`, we assume the inductive hypothesis, which says `∀ n_1 < n, ∃ (q r : Nat), n_1 = m * q + r ∧ r < m`.

```lean
theorem Example_6_4_1 : ∀ m > 0, ∀ (n : Nat),
    ∃ (q r : Nat), n = m * q + r ∧ r < m := by
  fix m : Nat
  assume h1 : m > 0
  by_strong_induc
  fix n : Nat
  assume ih : ∀ n_1 < n, ∃ (q r : Nat), n_1 = m * q + r ∧ r < m
  **done::
```

Our goal now is to prove that `∃ (q r : Nat), n = m * q + r ∧ r < m`.  Although strong induction does not require a base case, it is not uncommon for proofs by strong induction to involve reasoning by cases.  The proof in *HTPI* uses cases based on whether or not `n < m`.  If `n < m`, then the proof is easy: the numbers `q = 0` and `r​ = n` clearly have the required properties.  If `¬n < m`, then we can write `n` as `n = k + m`, for some natural number `k`.  Since `m > 0`, we have `k < n`, so we can apply the inductive hypothesis to `k`.  Notice that if `m > 1`, then `k` is not the number immediately preceding `n`; that's why this proof uses strong induction rather than ordinary induction.

How do we come up with the number `k` in the previous paragraph?  We'll use a theorem from Lean's library.  There are two slightly different versions of the theorem---notice that the first ends with `m + k` and the second ends with `k + m`:

::: {.ind}
```
@Nat.exists_eq_add_of_le : ∀ {m n : ℕ}, m ≤ n → ∃ (k : ℕ), n = m + k

@Nat.exists_eq_add_of_le' : ∀ {m n : ℕ}, m ≤ n → ∃ (k : ℕ), n = k + m
```
:::

We'll use the second version in our proof.

```lean
theorem Example_6_4_1 : ∀ m > 0, ∀ (n : Nat),
    ∃ (q r : Nat), n = m * q + r ∧ r < m := by
  fix m : Nat
  assume h1 : m > 0
  by_strong_induc
  fix n : Nat
  assume ih : ∀ n_1 < n, ∃ (q r : Nat), n_1 = m * q + r ∧ r < m
  by_cases h2 : n < m
  · -- Case 1. h2 : n < m
    apply Exists.intro 0
    apply Exists.intro n     --Goal : n = m * 0 + n ∧ n < m
    apply And.intro _ h2
    ring
    done
  · -- Case 2. h2 : ¬n < m
    have h3 : m ≤ n := by linarith
    obtain (k : Nat) (h4 : n = k + m) from Nat.exists_eq_add_of_le' h3
    have h5 : k < n := by linarith
    have h6 : ∃ (q r : Nat), k = m * q + r ∧ r < m := ih k h5
    obtain (q' : Nat)
      (h7 : ∃ (r : Nat), k = m * q' + r ∧ r < m) from h6
    obtain (r' : Nat) (h8 : k = m * q' + r' ∧ r' < m) from h7
    apply Exists.intro (q' + 1)
    apply Exists.intro r'     --Goal : n = m * (q' + 1) + r' ∧ r' < m
    apply And.intro _ h8.right
    show n = m * (q' + 1) + r' from
      calc n
        _ = k + m := h4
        _ = m * q' + r' + m := by rw [h8.left]
        _ = m * (q' + 1) + r' := by ring
    done
  done
```

The numbers `q` and `r` in `Example_6_4_1` are called the *quotient* and *remainder* when `n` is divided by `m`.  Lean knows how to compute these numbers: if `n` and `m` are natural numbers, then in Lean, `n / m` denotes the quotient when `n` is divided by `m`, and `n % m` denotes the remainder.  (The number `n % m` is also sometimes called `n` *modulo* `m`, or `n` *mod* `m`.)  And Lean knows theorems stating that these numbers have the properties specified in `Example_6_4_1`:

::: {.ind}
```
@Nat.div_add_mod : ∀ (m n : ℕ), n * (m / n) + m % n = m

@Nat.mod_lt : ∀ (x : ℕ) {y : ℕ}, y > 0 → x % y < y
```
:::

By the way, although we are unlikely to want to use the notation `n / 0` or `n % 0`, Lean uses the definitions `n / 0 = 0` and `n % 0 = n`.  As a result, the equation `n * (m / n) + m % n = m` is true even if `n = 0`.  That's why the theorem `Nat.div_add_mod` doesn't include a requirement that `n > 0`.  It is important to keep in mind that division of natural numbers is not the same as division of real numbers.  For example, dividing the natural number `5` by the natural number `2` gives a quotient of `2` (with a remainder of `1`), so `(5 : Nat) / (2 : Nat)` is `2`, but `(5 : Real) / (2 : Real)` is `2.5`.

There is also a strong form of recursion.  As an example of this, here is a recursive definition of a sequence of numbers called the *Fibonacci numbers*:

```lean
def Fib (n : Nat) : Nat :=
  match n with
    | 0 => 0
    | 1 => 1
    | k + 2 => Fib k + Fib (k + 1)
```

Notice that the formula for `Fib (k + 2)` involves the *two* previous values of `Fib`, not just the immediately preceding value.  That is the sense in which the recursion is *strong*.  Not surprisingly, theorems about the Fibonacci numbers are often proven by induction---either ordinary or strong.  We'll illustrate this with a proof by strong induction that `∀ (n : Nat), Fib n < 2 ^ n`.  This time we'll need to treat the cases `n = 0` and `n = 1` separately, since these values are treated separately in the definition of `Fib n`.  And we'll need to know that if `n` doesn't fall into either of those cases, then it falls into the third case: `n = k + 2` for some natural number `k`.  Since similar ideas will come up several times in the rest of this book, it will be useful to begin by proving lemmas that will help with this kind of reasoning.

We'll need two theorems from Lean's library, the second of which has two slightly different versions:

::: {.ind}
```
@Nat.pos_of_ne_zero : ∀ {n : ℕ}, n ≠ 0 → 0 < n

@lt_of_le_of_ne : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α},
                    a ≤ b → a ≠ b → a < b

@lt_of_le_of_ne' : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α},
                    a ≤ b → b ≠ a → a < b
```
:::

If we have `h1 : n ≠ 0`, then `Nat.pos_of_ne_zero h1` is a proof of `0 < n`.  But for natural numbers `a` and `b`, Lean treats `a < b` as meaning the same thing as `a + 1 ≤ b`, so this is also a proof of `1 ≤ n`.  If we also have `h2 : n ≠ 1`, then we can use `lt_of_le_of_ne'` to conclude `1 < n`, which is definitionally equal to `2 ≤ n`.  Combining this reasoning with the theorem `Nat.exists_eq_add_of_le'`, which we used in the last example, we can prove two lemmas that will be helpful for reasoning in which the first one or two natural numbers have to be treated separately.

```lean
lemma exists_eq_add_one_of_ne_zero {n : Nat}
    (h1 : n ≠ 0) : ∃ (k : Nat), n = k + 1 := by
  have h2 : 1 ≤ n := Nat.pos_of_ne_zero h1
  show ∃ (k : Nat), n = k + 1 from Nat.exists_eq_add_of_le' h2
  done

theorem exists_eq_add_two_of_ne_zero_one {n : Nat}
    (h1 : n ≠ 0) (h2 : n ≠ 1) : ∃ (k : Nat), n = k + 2 := by
  have h3 : 1 ≤ n := Nat.pos_of_ne_zero h1
  have h4 : 2 ≤ n := lt_of_le_of_ne' h3 h2
  show ∃ (k : Nat), n = k + 2 from Nat.exists_eq_add_of_le' h4
  done
```

With this preparation, we can present the proof:

```lean
example : ∀ (n : Nat), Fib n < 2 ^ n := by
  by_strong_induc
  fix n : Nat
  assume ih : ∀ n_1 < n, Fib n_1 < 2 ^ n_1
  by_cases h1 : n = 0
  · -- Case 1. h1 : n = 0
    rewrite [h1]   --Goal : Fib 0 < 2 ^ 0
    decide
    done
  · -- Case 2. h1 : ¬n = 0
    by_cases h2 : n = 1
    · -- Case 2.1. h2 : n = 1
      rewrite [h2]
      decide
      done
    · -- Case 2.2. h2 : ¬n = 1
      obtain (k : Nat) (h3 : n = k + 2) from
        exists_eq_add_two_of_ne_zero_one h1 h2
      have h4 : k < n := by linarith
      have h5 : Fib k < 2 ^ k := ih k h4
      have h6 : k + 1 < n := by linarith
      have h7 : Fib (k + 1) < 2 ^ (k + 1) := ih (k + 1) h6
      rewrite [h3]            --Goal : Fib (k + 2) < 2 ^ (k + 2)
      show Fib (k + 2) < 2 ^ (k + 2) from
        calc Fib (k + 2)
          _ = Fib k + Fib (k + 1) := by rfl
          _ < 2 ^ k + Fib (k + 1) := by rel [h5]
          _ < 2 ^ k + 2 ^ (k + 1) := by rel [h7]
          _ ≤ 2 ^ k + 2 ^ (k + 1) + 2 ^ k := by linarith
          _ = 2 ^ (k + 2) := by ring
      done
    done
  done
```

As with ordinary induction, strong induction can be useful for proving statements that do not at first seem to have the form `∀ (n : Nat), ...`.  To illustrate this, we'll prove the *well-ordering principle*, which says that if a set `S : Set Nat` is nonempty, then it has a smallest element.  We'll prove the contrapositive: if `S` has no smallest element, then it is empty.  To say that `S` is empty means `∀ (n : Nat), n ∉ S`, and that's the statement to which we will apply strong induction.

```lean
theorem well_ord_princ (S : Set Nat) : (∃ (n : Nat), n ∈ S) →
    ∃ n ∈ S, ∀ m ∈ S, n ≤ m := by
  contrapos
  assume h1 : ¬∃ n ∈ S, ∀ m ∈ S, n ≤ m
  quant_neg                   --Goal : ∀ (n : Nat), n ∉ S
  by_strong_induc
  fix n : Nat
  assume ih : ∀ n_1 < n, n_1 ∉ S  --Goal : n ∉ S
  contradict h1 with h2       --h2 : n ∈ S
    --Goal : ∃ n ∈ S, ∀ m ∈ S, n ≤ m
  apply Exists.intro n        --Goal : n ∈ S ∧ ∀ m ∈ S, n ≤ m
  apply And.intro h2          --Goal : ∀ m ∈ S, n ≤ m
  fix m : Nat
  assume h3 : m ∈ S
  have h4 : m < n → m ∉ S := ih m
  contrapos at h4             --h4 : m ∈ S → ¬m < n
  have h5 : ¬m < n := h4 h3
  linarith
  done
```

Section 6.4 of *HTPI* ends with an example of an application of the well-ordering principle.  The example gives a proof that $\sqrt{2}$ is irrational.  If $\sqrt{2}$ were rational, then there would be natural numbers $p$ and $q$ such that $q \ne 0$ and $p/q = \sqrt{2}$, and therefore $p^2 = 2q^2$.  So we can prove that $\sqrt{2}$ is irrational by showing that there do not exist natural numbers $p$ and $q$ such that $q \ne 0$ and $p^2 = 2q^2$.

The proof uses a definition from the exercises of Section 6.1:

```lean
def nat_even (n : Nat) : Prop := ∃ (k : Nat), n = 2 * k
```

We will also use the following lemma, whose proof we leave as an exercise for you:

```lean
lemma sq_even_iff_even (n : Nat) : nat_even (n * n) ↔ nat_even n := sorry
```

And we'll need another theorem that we haven't seen before:

::: {.ind}
```
@mul_left_cancel_iff_of_pos : ∀ {α : Type u_1} {a b c : α}
                    [inst : MulZeroClass α] [inst_1 : PartialOrder α]
                    [inst_2 : PosMulReflectLE α],
                    0 < a → (a * b = a * c ↔ b = c)
```
:::

To show that $\sqrt{2}$ is irrational, we will prove the statement

::: {.quote}
```
¬∃ (q p : Nat), p * p = 2 * (q * q) ∧ q ≠ 0
```
:::
We proceed by contradiction.  If this statement were false, then the set

::: {.quote}
```
S = {q : Nat | ∃ (p : Nat), p * p = 2 * (q * q) ∧ q ≠ 0}
```
:::

would be nonempty, and therefore, by the well-ordering principle, it would have a smallest element.  We then show that this leads to a contradiction.  Here is the proof.

```lean
theorem Theorem_6_4_5 :
    ¬∃ (q p : Nat), p * p = 2 * (q * q) ∧ q ≠ 0 := by
  set S : Set Nat :=
    {q : Nat | ∃ (p : Nat), p * p = 2 * (q * q) ∧ q ≠ 0}
  by_contra h1
  have h2 : ∃ (q : Nat), q ∈ S := h1
  have h3 : ∃ q ∈ S, ∀ r ∈ S, q ≤ r := well_ord_princ S h2
  obtain (q : Nat) (h4 : q ∈ S ∧ ∀ r ∈ S, q ≤ r) from h3
  have qinS : q ∈ S := h4.left
  have qleast : ∀ r ∈ S, q ≤ r := h4.right
  define at qinS     --qinS : ∃ (p : Nat), p * p = 2 * (q * q) ∧ q ≠ 0
  obtain (p : Nat) (h5 : p * p = 2 * (q * q) ∧ q ≠ 0) from qinS
  have pqsqrt2 : p * p = 2 * (q * q) := h5.left
  have qne0 : q ≠ 0 := h5.right
  have h6 : nat_even (p * p) := Exists.intro (q * q) pqsqrt2
  rewrite [sq_even_iff_even p] at h6    --h6 : nat_even p
  obtain (p' : Nat) (p'halfp : p = 2 * p') from h6
  have h7 : 2 * (2 * (p' * p')) = 2 * (q * q) := by
    rewrite [←pqsqrt2, p'halfp]
    ring
    done
  have h8 : 2 > 0 := by decide
  rewrite [mul_left_cancel_iff_of_pos h8] at h7
    --h7 : 2 * (p' * p') = q * q
  have h9 : nat_even (q * q) := Exists.intro (p' * p') h7.symm
  rewrite [sq_even_iff_even q] at h9   --h9 : nat_even q
  obtain (q' : Nat) (q'halfq : q = 2 * q') from h9
  have h10 : 2 * (p' * p') = 2 * (2 * (q' * q')) := by
    rewrite [h7, q'halfq]
    ring
    done
  rewrite [mul_left_cancel_iff_of_pos h8] at h10
    --h10 : p' * p' = 2 * (q' * q')
  have q'ne0 : q' ≠ 0 := by
    contradict qne0 with h11
    rewrite [q'halfq, h11]
    rfl
    done
  have q'inS : q' ∈ S := Exists.intro p' (And.intro h10 q'ne0)
  have qleq' : q ≤ q' := qleast q' q'inS
  rewrite [q'halfq] at qleq'        --qleq' : 2 * q' ≤ q'
  contradict q'ne0
  linarith
  done
```

### Exercises

::: {.numex arguments="1"}
```lean
--Hint: Use Exercise_6_1_16a1 and Exercise_6_1_16a2
--from the exercises of Section 6.1.
lemma sq_even_iff_even (n : Nat) :
    nat_even (n * n) ↔ nat_even n := sorry
```
:::

::: {.numex arguments="2"}
```lean
--This theorem proves that the square root of 6 is irrational
theorem Exercise_6_4_4a :
    ¬∃ (q p : Nat), p * p = 6 * (q * q) ∧ q ≠ 0 := sorry
```
:::

::: {.numex arguments="3"}
```lean
theorem Exercise_6_4_5 :
    ∀ n ≥ 12, ∃ (a b : Nat), 3 * a + 7 * b = n := sorry
```
:::

::: {.numex arguments="4"}
```lean
theorem Exercise_6_4_7a : ∀ (n : Nat),
    (Sum i from 0 to n, Fib i) + 1 = Fib (n + 2) := sorry
```
:::

::: {.numex arguments="5"}
```lean
theorem Exercise_6_4_7c : ∀ (n : Nat),
    Sum i from 0 to n, Fib (2 * i + 1) = Fib (2 * n + 2) := sorry
```
:::

::: {.numex arguments="6"}
```lean
theorem Exercise_6_4_8a : ∀ (m n : Nat),
    Fib (m + n + 1) = Fib m * Fib n + Fib (m + 1) * Fib (n + 1) := sorry
```
:::

::: {.numex arguments="7"}
```lean
theorem Exercise_6_4_8d : ∀ (m k : Nat), Fib m ∣ Fib (m * k) := sorry
```
Hint for \#7:  Let `m` be an arbitrary natural number, and then use induction on `k`.  For the induction step, you must prove `Fib m ∣ Fib (m * (k + 1))`.  If `m = 0 ∨ k = 0`, then this is easy.  If not, then use `exists_eq_add_one_of_ne_zero` to obtain a natural number `j` such that `m * k = j + 1`, and therefore `m * (k + 1) = j + m + 1`, and then apply `Exercise_6_4_8a`.
:::

::: {.numex arguments="8"}
```lean
def Fib_like (n : Nat) : Nat :=
  match n with
    | 0 => 1
    | 1 => 2
    | k + 2 => 2 * (Fib_like k) + Fib_like (k + 1)

theorem Fib_like_formula : ∀ (n : Nat), Fib_like n = 2 ^ n := sorry
```
:::

::: {.numex arguments="9"}
```lean
def triple_rec (n : Nat) : Nat :=
  match n with
    | 0 => 0
    | 1 => 2
    | 2 => 4
    | k + 3 => 4 * triple_rec k +
                6 * triple_rec (k + 1) + triple_rec (k + 2)

theorem triple_rec_formula :
    ∀ (n : Nat), triple_rec n = 2 ^ n * Fib n := sorry
```
:::

10\. In this exercise you will prove that the numbers `q` and `r` in `Example_6_4_1` are unique.  It is helpful to prove a lemma first.
```lean
lemma quot_rem_unique_lemma {m q r q' r' : Nat}
    (h1 : m * q + r = m * q' + r') (h2 : r' < m) : q ≤ q' := sorry

theorem quot_rem_unique (m q r q' r' : Nat)
    (h1 : m * q + r = m * q' + r') (h2 : r < m) (h3 : r' < m) :
    q = q' ∧ r = r' := sorry
```

11\. Use the theorem in the previous exercise to prove the following characterization of `n / m` and `n % m`.
```lean
theorem div_mod_char (m n q r : Nat)
    (h1 : n = m * q + r) (h2 : r < m) : q = n / m ∧ r = n % m := sorry
```

## 6.5. Closures Again

Section 6.5 of *HTPI* gives one more application of recursion and induction: another proof of the existence of closures of sets under functions.  Recall from Section 5.4 that if `f : A → A` and `B : Set A`, then the *closure* of `B` under `f` is the smallest set containing `B` that is closed under `f`.  In Section 5.4, we constructed the closure of `B` under `f` by taking the intersection of all sets containing `B` that are closed under `f`.  In this section, we construct the closure by starting with the set `B` and repeatedly taking the image under `f`.  For the motivation for this strategy, see *HTPI*; here we focus on how to carry out this strategy in Lean.

To talk about repeatedly taking the image of a set under a function, we will need a recursive definition:

```lean
def rep_image {A : Type} (f : A → A) (n : Nat) (B : Set A) : Set A :=
  match n with
    | 0 => B
    | k + 1 => image f (rep_image f k B)
```

According to this definition, `rep_image f 0 B = B`, `rep_image f 1 B = image f B`, `rep_image f 2 B = image f (image f B)`, and so on.  In other words, `rep_image f n B` is the result of starting with `B` and then taking the image under `f` `n` times.  To make it easier to work with this definition, we state two simple theorems, both of which follow immediately from the definition.

```lean
theorem rep_image_base {A : Type} (f : A → A) (B : Set A) :
    rep_image f 0 B = B := by rfl

theorem rep_image_step {A : Type} (f : A → A) (n : Nat) (B : Set A) :
    rep_image f (n + 1) B = image f (rep_image f n B) := by rfl
```

We will prove that the closure of `B` under `f` is the union of the sets `rep_image f n B`.  We will call this the *cumulative image* of `B` under `f`, and we define it as follows:

```lean
def cumul_image {A : Type} (f : A → A) (B : Set A) : Set A :=
  {x : A | ∃ (n : Nat), x ∈ rep_image f n B}
```

To prove that `cumul_image f B` is the closure of `B` under `f`, we first prove a lemma saying that if `B ⊆ D` and `D` is closed under `f`, then for every natural number `n`, `rep_image f n B ⊆ D`.  We prove it by induction.

```lean
lemma rep_image_sub_closed {A : Type} {f : A → A} {B D : Set A}
    (h1 : B ⊆ D) (h2 : closed f D) :
    ∀ (n : Nat), rep_image f n B ⊆ D := by
  by_induc
  · -- Base Case
    rewrite [rep_image_base]          --Goal : B ⊆ D
    show B ⊆ D from h1
    done
  · -- Induction Step
    fix n : Nat
    assume ih : rep_image f n B ⊆ D   --Goal : rep_image f (n + 1) B ⊆ D
    fix x : A
    assume h3 : x ∈ rep_image f (n + 1) B  --Goal : x ∈ D
    rewrite [rep_image_step] at h3
    define at h3    --h3 : ∃ x_1 ∈ rep_image f n B, f x_1 = x
    obtain (b : A) (h4 : b ∈ rep_image f n B ∧ f b = x) from h3
    rewrite [←h4.right]   --Goal : f b ∈ D    
    have h5 : b ∈ D := ih h4.left
    define at h2          --h2 : ∀ x ∈ D, f x ∈ D
    show f b ∈ D from h2 b h5
    done
  done
```

With this preparation, we can now prove that `cumul_image f B` is the closure of `B` under `f`.

```lean
theorem Theorem_6_5_1 {A : Type} (f : A → A) (B : Set A) :
    closure f B (cumul_image f B) := by
  define
  apply And.intro
  · -- Proof that cumul_image f B ∈ {D : Set A | B ⊆ D ∧ closed f D}
    define  --Goal : B ⊆ cumul_image f B ∧ closed f (cumul_image f B)
    apply And.intro
    · -- Proof that B ⊆ cumul_image f B
      fix x : A
      assume h1 : x ∈ B
      define     --Goal : ∃ (n : Nat), x ∈ rep_image f n B
      apply Exists.intro 0
      rewrite [rep_image_base]  --Goal : x ∈ B
      show x ∈ B from h1
      done
    · -- Proof that cumul_image f B closed under f
      define
      fix x : A
      assume h1 : x ∈ cumul_image f B  --Goal : f x ∈ cumul_image f B
      define at h1
      obtain (m : Nat) (h2 : x ∈ rep_image f m B) from h1
      define     --Goal : ∃ (n : Nat), f x ∈ rep_image f n B
      apply Exists.intro (m + 1) --Goal : f x ∈ rep_image f (m + 1) B
      rewrite [rep_image_step]   --Goal : f x ∈ image f (rep_image f m B)
      define     --Goal : ∃ x_1 ∈ rep_image f m B, f x_1 = f x
      apply Exists.intro x  --Goal : x ∈ rep_image f m B ∧ f x = f x
      apply And.intro h2
      rfl
      done
    done
  · -- Proof that cumul_image f B is smallest
    fix D : Set A
    assume h1 : D ∈ {D : Set A | B ⊆ D ∧ closed f D}
    define at h1  --h1 : B ⊆ D ∧ closed f D
    define   --Goal : ∀ ⦃a : A⦄, a ∈ cumul_image f B → a ∈ D
    fix x : A
    assume h2 : x ∈ cumul_image f B  --Goal : x ∈ D
    define at h2  --h2: ∃ (n : Nat), x ∈ rep_image f n B
    obtain (m : Nat) (h3 : x ∈ rep_image f m B) from h2
    have h4 : rep_image f m B ⊆ D :=
      rep_image_sub_closed h1.left h1.right m
    show x ∈ D from h4 h3
    done
  done
```

### Exercises

1\. Recall the following definitions from the exercises of Section 5.4:

```lean
def closed_family {A : Type} (F : Set (A → A)) (C : Set A) : Prop :=
  ∀ f ∈ F, closed f C

def closure_family {A : Type} (F : Set (A → A)) (B C : Set A) : Prop :=
  smallestElt (sub A) C {D : Set A | B ⊆ D ∧ closed_family F D}
```

These definitions say that a set is closed under a family of functions if it is closed under all of the functions in the family, and the closure of a set `B` under a family of functions is the smallest set containing `B` that is closed under the family.

In this exercise we will use the following additional definitions:

```lean
def rep_image_family {A : Type}
    (F : Set (A → A)) (n : Nat) (B : Set A) : Set A :=
  match n with
    | 0 => B
    | k + 1 => {x : A | ∃ f ∈ F, x ∈ image f (rep_image_family F k B)}

def cumul_image_family {A : Type}
    (F : Set (A → A)) (B : Set A) : Set A :=
  {x : A | ∃ (n : Nat), x ∈ rep_image_family F n B}
```

The following theorems establish that if `F : Set (A → A)` and `B : Set A`, then `cumul_image_family F B` is the closure of `B` under `F`.  The first two are proven by `rfl`; the other two are for you to prove.

```lean
theorem rep_image_family_base {A : Type}
    (F : Set (A → A)) (B : Set A) : rep_image_family F 0 B = B := by rfl

theorem rep_image_family_step {A : Type}
    (F : Set (A → A)) (n : Nat) (B : Set A) :
    rep_image_family F (n + 1) B =
    {x : A | ∃ f ∈ F, x ∈ image f (rep_image_family F n B)} := by rfl

lemma rep_image_family_sub_closed {A : Type}
    (F : Set (A → A)) (B D : Set A)
    (h1 : B ⊆ D) (h2 : closed_family F D) :
    ∀ (n : Nat), rep_image_family F n B ⊆ D := sorry

theorem Exercise_6_5_3 {A : Type} (F : Set (A → A)) (B : Set A) :
    closure_family F B (cumul_image_family F B) := sorry
```

::: {.mdsk}
:::

The next two exercises concern the following two definitions from Section 5.4:

```lean
def closed2 {A : Type} (f : A → A → A) (C : Set A) : Prop :=
  ∀ x ∈ C, ∀ y ∈ C, f x y ∈ C

def closure2 {A : Type} (f : A → A → A) (B C : Set A) : Prop := 
  smallestElt (sub A) C {D : Set A | B ⊆ D ∧ closed2 f D}
```

They also use the following definition, which extends the idea of the image of a set under a function to functions of two variables:

```lean
def image2 {A : Type} (f : A → A → A) (B : Set A) : Set A :=
  {z : A | ∃ (x y : A), x ∈ B ∧ y ∈ B ∧ z = f x y}
```

2\. A natural way to try to find the closure of a set under a function of two variables would be to use the following definitions and theorems:

```lean
def rep_image2 {A : Type}
    (f : A → A → A) (n : Nat) (B : Set A) : Set A :=
  match n with
    | 0 => B
    | k + 1 => image2 f (rep_image2 f k B)

theorem rep_image2_base {A : Type} (f : A → A → A) (B : Set A) :
    rep_image2 f 0 B = B := by rfl

theorem rep_image2_step {A : Type}
    (f : A → A → A) (n : Nat) (B : Set A) :
    rep_image2 f (n + 1) B = image2 f (rep_image2 f n B) := by rfl

def cumul_image2 {A : Type} (f : A → A → A) (B : Set A) : Set A :=
  {x : A | ∃ (n : Nat), x ∈ rep_image2 f n B}
```

We could now try to prove that if `f : A → A → A` and `B : Set A`, then `cumul_image2 f B` is the closure of `B` under `f`.  However, this approach doesn't work, because `cumul_image2 f B` might not be closed under `f`.

Here is an incorrect informal argument that `cumul_image2 f B` is closed under `f`.  Suppose `x` and `y` are elements of `cumul_image2 f B`.  This means that we can choose some natural number `n` such that `x ∈ rep_image2 f n B` and `y ∈ rep_image2 f n B`.  This implies that `f x y ∈ image2 f (rep_image2 f n B) = rep_image2 f (n + 1) B`, so `f x y ∈ cumul_image2 f B`.

Find the mistake in this informal argument by trying to turn it into a proof in Lean:

```lean
--You won't be able to complete this proof
theorem Exercise_6_5_6 {A : Type} (f : A → A → A) (B : Set A) :
    closed2 f (cumul_image2 f B) := sorry
```

3\. In this exercise, we fix the mistake in the attempted proof in the previous exercise.  Instead of repeatedly taking the image of a set, we repeatedly take the union of a set with its image:

```lean
def un_image2 {A : Type} (f : A → A → A) (B : Set A) : Set A :=
  B ∪ (image2 f B)

def rep_un_image2 {A : Type}
    (f : A → A → A) (n : Nat) (B : Set A) : Set A :=
  match n with
    | 0 => B
    | k + 1 => un_image2 f (rep_un_image2 f k B)

theorem rep_un_image2_base {A : Type} (f : A → A → A) (B : Set A) :
    rep_un_image2 f 0 B = B := by rfl

theorem rep_un_image2_step {A : Type}
    (f : A → A → A) (n : Nat) (B : Set A) :
    rep_un_image2 f (n + 1) B =
    un_image2 f (rep_un_image2 f n B) := by rfl

def cumul_un_image2 {A : Type}
    (f : A → A → A) (B : Set A) : Set A :=
  {x : A | ∃ (n : Nat), x ∈ rep_un_image2 f n B}
```

Now prove that if `f : A → A → A` and `B : Set A`, then `cumul_un_image2 f B` is the closure of `B` under `f` by completing the following proofs:

```lean
theorem Exercise_6_5_8a {A : Type} (f : A → A → A) (B : Set A) :
    ∀ (m n : Nat), m ≤ n →
    rep_un_image2 f m B ⊆ rep_un_image2 f n B := sorry

lemma rep_un_image2_sub_closed {A : Type} {f : A → A → A} {B D : Set A}
    (h1 : B ⊆ D) (h2 : closed2 f D) :
    ∀ (n : Nat), rep_un_image2 f n B ⊆ D := sorry

lemma closed_lemma
    {A : Type} {f : A → A → A} {B : Set A} {x y : A} {nx ny n : Nat}
    (h1 : x ∈ rep_un_image2 f nx B) (h2 : y ∈ rep_un_image2 f ny B)
    (h3 : nx ≤ n) (h4 : ny ≤ n) :
    f x y ∈ cumul_un_image2 f B := sorry

theorem Exercise_6_5_8b {A : Type} (f : A → A → A) (B : Set A) :
    closure2 f B (cumul_un_image2 f B) := sorry
```

::: {.mdsk}
:::

The remaining exercises in this section use the following definitions:

```lean
def idExt (A : Type) : Set (A × A) := {(x, y) : A × A | x = y}

def rep_comp {A : Type} (R : Set (A × A)) (n : Nat) : Set (A × A) :=
  match n with
    | 0 => idExt A
    | k + 1 => comp (rep_comp R k) R

def cumul_comp {A : Type} (R : Set (A × A)) : Set (A × A) :=
  {(x, y) : A × A | ∃ n ≥ 1, (x, y) ∈ rep_comp R n}
```

::: {.numex arguments="4"}
```lean
theorem rep_comp_one {A : Type} (R : Set (A × A)) :
    rep_comp R 1 = R := sorry
```
:::

::: {.numex arguments="5"}
```lean
theorem Exercise_6_5_11 {A : Type} (R : Set (A × A)) :
    ∀ (m n : Nat), rep_comp R (m + n) =
    comp (rep_comp R m) (rep_comp R n) := sorry
```
:::

::: {.numex arguments="6"}
```lean
lemma rep_comp_sub_trans {A : Type} {R S : Set (A × A)}
    (h1 : R ⊆ S) (h2 : transitive (RelFromExt S)) :
    ∀ n ≥ 1, rep_comp R n ⊆ S := sorry
```
:::

::: {.numex arguments="7"}
```lean
theorem Exercise_6_5_14 {A : Type} (R : Set (A × A)) :
    smallestElt (sub (A × A)) (cumul_comp R)
    {S : Set (A × A) | R ⊆ S ∧ transitive (RelFromExt S)} := sorry
```
:::