Chap7.qmd

# Number Theory

## 7.1.  Greatest Common Divisors

The proofs in this chapter and the next are significantly longer than those in previous chapters.  As a result, we will skip some details in the text, leaving proofs of a number of theorems as exercises for you.  The most interesting of these exercises are included in the exercise lists at the ends of the sections; for the rest, you can compare your solutions to proofs that can be found in the Lean package that accompanies this book.  Also, we will occasionally use theorems that we have not used before without explanation.  If necessary, you can use `#check` to look up what they say.

Section 7.1 of *HTPI* introduces the Euclidean algorithm for computing the greatest common divisor (gcd) of two positive integers $a$ and $b$.  The motivation for the algorithm is the fact that if $r$ is the remainder when $a$ is divided by $b$, then any natural number that divides both $a$ and $b$ also divides $r$, and any natural number that divides both $b$ and $r$ also divides $a$.

Let's prove these statements in Lean.  Recall that in Lean, the remainder when `a` is divided by `b` is called `a` mod `b`, and it is denoted `a % b`.  We'll prove the first statement, and leave the second as an exercise for you.  It will be convenient for our work with greatest common divisors in Lean to let `a` and `b` be natural numbers rather than positive integers (thus allowing either of them to be zero).  

```lean
theorem dvd_mod_of_dvd_a_b {a b d : Nat}
    (h1 : d ∣ a) (h2 : d ∣ b) : d ∣ (a % b) := by
  set q : Nat := a / b
  have h3 : b * q + a % b = a := Nat.div_add_mod a b
  obtain (j : Nat) (h4 : a = d * j) from h1
  obtain (k : Nat) (h5 : b = d * k) from h2
  define    --Goal : ∃ (c : Nat), a % b = d * c
  apply Exists.intro (j - k * q)
  show a % b = d * (j - k * q) from
    calc a % b
      _ = b * q + a % b - b * q := (Nat.add_sub_cancel_left _ _).symm
      _ = a - b * q := by rw [h3]
      _ = d * j - d * (k * q) := by rw [h4, h5, mul_assoc]
      _ = d * (j - k * q) := (Nat.mul_sub_left_distrib _ _ _).symm
  done

theorem dvd_a_of_dvd_b_mod {a b d : Nat}
    (h1 : d ∣ b) (h2 : d ∣ (a % b)) : d ∣ a := sorry
```

These theorems tell us that the gcd of `a` and `b` is the same as the gcd of `b` and `a % b`, which suggests that the following recursive definition should compute the gcd of `a` and `b`:

```lean
def **gcd:: (a b : Nat) : Nat :=
  match b with
    | 0 => a
    | n + 1 => gcd (n + 1) (a % (n + 1))
```

Unfortunately, Lean puts a red squiggle under `gcd`, and it displays in the Infoview a long error message that begins `fail to show termination`.  What is Lean complaining about?

The problem is that recursive definitions are dangerous.  To understand the danger, consider the following recursive definition:

```lean
def loop (n : Nat) : Nat := loop (n + 1)
```

Suppose we try to use this definition to compute `loop 3`.  The definition would lead us to perform the following calculation:

::: {.ind}
```
loop 3 = loop 4 = loop 5 = loop 6 = ...
```
:::

Clearly this calculation will go on forever and will never produce an answer.  So the definition of `loop` does not actually succeed in defining a function from `Nat` to `Nat`.

Lean insists that recursive definitions must avoid such nonterminating calculations.  Why did it accept all of our previous recursive definitions?  The reason is that in each case, the definition of the value of the function at a natural number `n` referred only to values of the function at numbers smaller than `n`.  Since a decreasing list of natural numbers cannot go on forever, such definitions lead to calculations that are guaranteed to terminate.

What about our recursive definition of `gcd a b`?  This function has two arguments, `a` and `b`, and when `b = n + 1`, the definition asks us to compute `gcd (n + 1) (a % (n + 1))`.  The first argument here could actually be larger than the first argument in the value we are trying to compute, `gcd a b`.  But the second argument will always be smaller, and that will suffice to guarantee that the calculation terminates.  We can tell Lean to focus on the second argument `b` by adding a `termination_by` clause to the end of our recursive definition:

```lean
def gcd (a b : Nat) : Nat :=
  match b with
    | 0 => a
    | n + 1 => **gcd (n + 1) (a % (n + 1))::
  termination_by b
```

Unfortunately, Lean still isn't satisfied, but the error message this time is more helpful.  The message says that Lean failed to prove termination, and at the end of the message it says that the goal it failed to prove is `a % (n + 1) < n + 1`, which is precisely what is needed to show that the second argument of `gcd (n + 1) (a % (n + 1))` is smaller than the second argument of `gcd a b` when `b = n + 1`.  We'll need to provide a proof of this goal to convince Lean to accept our recursive definition.  Fortunately, it's not hard to prove:

```lean
lemma mod_succ_lt (a n : Nat) : a % (n + 1) < n + 1 := by
  have h : n + 1 > 0 := Nat.succ_pos n
  show a % (n + 1) < n + 1 from Nat.mod_lt a h
  done
```

Lean's error message suggests several ways to fix the problem with our recursive definition.  We'll use the first suggestion:  ``Use `have`-expressions to prove the remaining goals``.  Here, finally, is the definition of `gcd` that Lean is willing to accept.  (You can ignore the initial line `@[semireducible]`.  For technical reasons that we won't go into, this line is needed to make this complicated recursive definition work in proofs the same way that our previous, simpler recursive definitions did.)

```lean
@[semireducible]
def gcd (a b : Nat) : Nat :=
  match b with
    | 0 => a
    | n + 1 =>
      have : a % (n + 1) < n + 1 := mod_succ_lt a n
      gcd (n + 1) (a % (n + 1))
  termination_by b
```

Notice that in the `have` expression, we have not bothered to specify an identifier for the assertion being proven, since we never need to refer to it.  Let's try out our `gcd` function:

```lean
++#eval:: gcd 672 161    --Answer: 7.  Note 672 = 7 * 96 and 161 = 7 * 23.
```

To establish the main properties of `gcd a b` we'll need several lemmas.  We prove some of them and leave others as exercises.

```lean
lemma gcd_base (a : Nat) : gcd a 0 = a := by rfl

lemma gcd_nonzero (a : Nat) {b : Nat} (h : b ≠ 0) :
    gcd a b = gcd b (a % b) := by
  obtain (n : Nat) (h2 : b = n + 1) from exists_eq_add_one_of_ne_zero h
  rewrite [h2]   --Goal : gcd a (n + 1) = gcd (n + 1) (a % (n + 1))
  rfl
  done

lemma mod_nonzero_lt (a : Nat) {b : Nat} (h : b ≠ 0) : a % b < b := sorry

lemma dvd_self (n : Nat) : n ∣ n := sorry
```

One of the most important properties of `gcd a b` is that it divides both `a` and `b`.  We prove it by strong induction on `b`.

```lean
theorem gcd_dvd : ∀ (b a : Nat), (gcd a b) ∣ a ∧ (gcd a b) ∣ b := by
  by_strong_induc
  fix b : Nat
  assume ih : ∀ b_1 < b, ∀ (a : Nat), (gcd a b_1) ∣ a ∧ (gcd a b_1) ∣ b_1
  fix a : Nat
  by_cases h1 : b = 0
  · -- Case 1. h1 : b = 0
    rewrite [h1, gcd_base]   --Goal: a ∣ a ∧ a ∣ 0
    apply And.intro (dvd_self a)
    define
    apply Exists.intro 0
    rfl
    done
  · -- Case 2. h1 : b ≠ 0
    rewrite [gcd_nonzero a h1]
      --Goal : gcd b (a % b) ∣ a ∧ gcd b (a % b) ∣ b
    have h2 : a % b < b := mod_nonzero_lt a h1
    have h3 : (gcd b (a % b)) ∣ b ∧ (gcd b (a % b)) ∣ (a % b) :=
      ih (a % b) h2 b
    apply And.intro _ h3.left
    show (gcd b (a % b)) ∣ a from dvd_a_of_dvd_b_mod h3.left h3.right
    done
  done
```

You may wonder why we didn't start the proof like this:

```lean
theorem gcd_dvd : ∀ (a b : Nat), (gcd a b) ∣ a ∧ (gcd a b) ∣ b := by
  fix a : Nat
  by_strong_induc
  fix b : Nat
  assume ih : ∀ b_1 < b, (gcd a b_1) ∣ a ∧ (gcd a b_1) ∣ b_1
```

In fact, this approach wouldn't have worked.  It is an interesting exercise to try to complete this version of the proof and see why it fails.

Another interesting question is why we asserted both `(gcd a b) ∣ a` and `(gcd a b) ∣ b` in the same theorem.  Wouldn't it have been easier to give separate proofs of the statements `∀ (b a : Nat), (gcd a b) ∣ a` and `∀ (b a : Nat), (gcd a b) ∣ b`?  Again, you might find it enlightening to see why that wouldn't have worked.  However, now that we have proven both divisibility statements, we can state them as separate theorems:

```lean
theorem gcd_dvd_left (a b : Nat) : (gcd a b) ∣ a := (gcd_dvd b a).left

theorem gcd_dvd_right (a b : Nat) : (gcd a b) ∣ b := (gcd_dvd b a).right
```

Next we turn to Theorem 7.1.4 in *HTPI*, which says that there are integers $s$ and $t$ such that $\text{gcd}(a, b) = s a + t b$.  (We say that $\text{gcd}(a, b)$ can be written as a *linear combination* of $a$ and $b$.)  In *HTPI*, this is proven by using an extended version of the Euclidean algorithm to compute the coefficients $s$ and $t$.  Here we will use a different recursive procedure to compute $s$ and $t$.  If $b = 0$, then $\text{gcd}(a, b) = a = 1 \cdot a + 0 \cdot b$, so we can use the values $s = 1$ and $t = 0$.  Otherwise, let $q$ and $r$ be the quotient and remainder when $a$ is divided by $b$.  Then $a = bq + r$ and $\text{gcd}(a, b) = \text{gcd}(b, r)$.  Now suppose that we have already computed integers $s'$ and $t'$ such that
$$
\text{gcd}(b, r) = s' b + t' r.
$$
Then
\begin{align*}
\text{gcd}(a, b) &= \text{gcd}(b, r) = s' b + t' r\\
&= s' b + t' (a - bq) = t' a + (s' - t'q)b.
\end{align*}
Thus, to write $\text{gcd}(a, b) = s a + t b$ we can use the values
\begin{equation}\tag{$*$}
s = t', \qquad t = s' - t'q.
\end{equation}

We will use these equations as the basis for recursive definitions of Lean functions `gcd_c1` and `gcd_c2` such that the required coefficients can be obtained from the formulas `s = gcd_c1 a b` and `t = gcd_c2 a b`.  Notice that `s` and `t` could be negative, so they must have type `Int`, not `Nat`.  As a result, in definitions and theorems involving `gcd_c1` and `gcd_c2` we will sometimes have to deal with coercion of natural numbers to integers.

The functions `gcd_c1` and `gcd_c2` will be *mutually recursive*; in other words, each will be defined not only in terms of itself but also in terms of the other.  Fortunately, Lean allows for such mutual recursion.  Here are the definitions we will use.

```lean
mutual
  @[semireducible]
  def gcd_c1 (a b : Nat) : Int :=
    match b with
      | 0 => 1
      | n + 1 =>
        have : a % (n + 1) < n + 1 := mod_succ_lt a n
        gcd_c2 (n + 1) (a % (n + 1))
          --Corresponds to s = t'
    termination_by b

  @[semireducible]
  def gcd_c2 (a b : Nat) : Int :=
    match b with
      | 0 => 0
      | n + 1 =>
        have : a % (n + 1) < n + 1 := mod_succ_lt a n
        gcd_c1 (n + 1) (a % (n + 1)) -
          (gcd_c2 (n + 1) (a % (n + 1))) * ↑(a / (n + 1))
          --Corresponds to t = s' - t'q
    termination_by b
end
```

Notice that in the definition of `gcd_c2`, the quotient `a / (n + 1)` is computed using natural-number division, but it is then coerced to be an integer so that it can be multiplied by the integer `gcd_c2 (n + 1) (a % (n + 1))`.

Our main theorem about these functions is that they give the coefficients needed to write `gcd a b` as a linear combination of `a` and `b`.  As usual, stating a few lemmas first helps with the proof.  We leave the proofs of two of them as exercises for you (hint: imitate the proof of `gcd_nonzero` above).

```lean
lemma gcd_c1_base (a : Nat) : gcd_c1 a 0 = 1 := by rfl

lemma gcd_c1_nonzero (a : Nat) {b : Nat} (h : b ≠ 0) :
    gcd_c1 a b = gcd_c2 b (a % b) := sorry

lemma gcd_c2_base (a : Nat) : gcd_c2 a 0 = 0 := by rfl

lemma gcd_c2_nonzero (a : Nat) {b : Nat} (h : b ≠ 0) :
    gcd_c2 a b = gcd_c1 b (a % b) - (gcd_c2 b (a % b)) * ↑(a / b) := sorry
```

With that preparation, we are ready to prove that `gcd_c1 a b` and `gcd_c2 a b` give coefficients for expressing `gcd a b` as a linear combination of `a` and `b`.  Of course, the theorem is proven by strong induction.  For clarity, we'll write the coercions explicitly in this proof.  We'll make a few comments after the proof that may help you follow the details.

```lean
theorem gcd_lin_comb : ∀ (b a : Nat),
    (gcd_c1 a b) * ↑a + (gcd_c2 a b) * ↑b = ↑(gcd a b) := by
  by_strong_induc
  fix b : Nat
  assume ih : ∀ b_1 < b, ∀ (a : Nat),
    (gcd_c1 a b_1) * ↑a + (gcd_c2 a b_1) * ↑b_1 = ↑(gcd a b_1)
  fix a : Nat
  by_cases h1 : b = 0
  · -- Case 1. h1 : b = 0
    rewrite [h1, gcd_c1_base, gcd_c2_base, gcd_base]
      --Goal : 1 * ↑a + 0 * ↑0 = ↑a
    ring
    done
  · -- Case 2. h1 : b ≠ 0
    rewrite [gcd_c1_nonzero a h1, gcd_c2_nonzero a h1, gcd_nonzero a h1]
      --Goal : gcd_c2 b (a % b) * ↑a +
      -- (gcd_c1 b (a % b) - gcd_c2 b (a % b) * ↑(a / b)) * ↑b =
      -- ↑(gcd b (a % b))
    set r : Nat := a % b
    set q : Nat := a / b
    set s : Int := gcd_c1 b r
    set t : Int := gcd_c2 b r
      --Goal : t * ↑a + (s - t * ↑q) * ↑b = ↑(gcd b r)
    have h2 : r < b := mod_nonzero_lt a h1
    have h3 : s * ↑b + t * ↑r = ↑(gcd b r) := ih r h2 b
    have h4 : b * q + r = a := Nat.div_add_mod a b
    rewrite [←h3, ←h4]
    rewrite [Nat.cast_add, Nat.cast_mul]
      --Goal : t * (↑b * ↑q + ↑r) + (s - t * ↑q) * ↑b = s * ↑b + t * ↑r
    ring
    done
  done
```

In case 2, we have introduced the variables `r`, `q`, `s`, and `t` to simplify the notation.  Notice that the `set` tactic automatically plugs in this notation in the goal.  After the step `rewrite [←h3, ←h4]`, the goal contains the expression `↑(b * q + r)`.  You can use the `#check` command to see why `Nat.cast_add` and `Nat.cast_mul` convert this expression to first `↑(b * q) + ↑r` and then `↑b * ↑q + ↑r`.  Without those steps, the `ring` tactic would not have been able to complete the proof.

We can try out the functions `gcd_c1` and `gcd_c2` as follows:

```lean
++#eval:: gcd_c1 672 161  --Answer: 6
++#eval:: gcd_c2 672 161  --Answer: -25
  --Note 6 * 672 - 25 * 161 = 4032 - 4025 = 7 = gcd 672 161
```

Finally, we turn to Theorem 7.1.6 in *HTPI*, which expresses one of the senses in which `gcd a b` is the *greatest* common divisor of `a` and `b`.  Our proof follows the strategy of the proof in *HTPI*, with one additional step: we begin by using the theorem `Int.natCast_dvd_natCast` to change the goal from `d ∣ gcd a b` to `↑d ∣ ↑(gcd a b)` (where the coercions are from `Nat` to `Int`), so that the rest of the proof can work with integer algebra rather than natural-number algebra.

```lean
theorem Theorem_7_1_6 {d a b : Nat} (h1 : d ∣ a) (h2 : d ∣ b) :
    d ∣ gcd a b := by
  rewrite [←Int.natCast_dvd_natCast]    --Goal : ↑d ∣ ↑(gcd a b)
  set s : Int := gcd_c1 a b
  set t : Int := gcd_c2 a b
  have h3 : s * ↑a + t * ↑b = ↑(gcd a b) := gcd_lin_comb b a
  rewrite [←h3]                 --Goal : ↑d ∣ s * ↑a + t * ↑b
  obtain (j : Nat) (h4 : a = d * j) from h1
  obtain (k : Nat) (h5 : b = d * k) from h2
  rewrite [h4, h5, Nat.cast_mul, Nat.cast_mul]
    --Goal : ↑d ∣ s * (↑d * ↑j) + t * (↑d * ↑k)
  define
  apply Exists.intro (s * ↑j + t * ↑k)
  ring
  done
```

We will ask you in the exercises to prove that, among the common divisors of `a` and `b`, `gcd a b` is the greatest with respect to the usual ordering of the natural numbers (as long as `gcd a b ≠ 0`).

### Exercises

::: {.numex arguments="1"}
```lean
theorem dvd_a_of_dvd_b_mod {a b d : Nat}
    (h1 : d ∣ b) (h2 : d ∣ (a % b)) : d ∣ a := sorry
```
:::

::: {.numex arguments="2"}
```lean
lemma gcd_comm_lt {a b : Nat} (h : a < b) : gcd a b = gcd b a := sorry

theorem gcd_comm (a b : Nat) : gcd a b = gcd b a := sorry
```
:::

::: {.numex arguments="3"}
```lean
theorem Exercise_7_1_5 (a b : Nat) (n : Int) :
    (∃ (s t : Int), s * a + t * b = n) ↔ (↑(gcd a b) : Int) ∣ n := sorry
```
:::

::: {.numex arguments="4"}
```lean
theorem Exercise_7_1_6 (a b c : Nat) :
    gcd a b = gcd (a + b * c) b := sorry
```
:::

::: {.numex arguments="5"}
```lean
theorem gcd_is_nonzero {a b : Nat} (h : a ≠ 0 ∨ b ≠ 0) :
    gcd a b ≠ 0 := sorry
```
:::

::: {.numex arguments="6"}
```lean
theorem gcd_greatest {a b d : Nat} (h1 : gcd a b ≠ 0)
    (h2 : d ∣ a) (h3 : d ∣ b) : d ≤ gcd a b := sorry
```
:::

::: {.numex arguments="7"}
```lean
lemma Lemma_7_1_10a {a b : Nat}
    (n : Nat) (h : a ∣ b) : (n * a) ∣ (n * b) := sorry

lemma Lemma_7_1_10b {a b n : Nat}
    (h1 : n ≠ 0) (h2 : (n * a) ∣ (n * b)) : a ∣ b := sorry

lemma Lemma_7_1_10c {a b : Nat}
    (h1 : a ∣ b) (h2 : b ∣ a) : a = b := sorry

theorem Exercise_7_1_10 (a b n : Nat) :
    gcd (n * a) (n * b) = n * gcd a b := sorry
```
:::

## 7.2.  Prime Factorization

A natural number $n$ is said to be *prime* if it is at least 2 and it cannot be written as a product of two smaller natural numbers.  Of course, we can write this definition in Lean.

```lean
def prime (n : Nat) : Prop :=
  2 ≤ n ∧ ¬∃ (a b : Nat), a * b = n ∧ a < n ∧ b < n
```

The main goal of Section 7.2 of *HTPI* is to prove that every positive integer has a unique prime factorization; that is, it can be written in a unique way as the product of a nondecreasing list of prime numbers.  To get started on this goal, we first prove that every number greater than or equal to 2 has a prime factor.  We leave one lemma as an exercise for you (it is a natural-number version of `Theorem_3_3_7`).

```lean
def prime_factor (p n : Nat) : Prop := prime p ∧ p ∣ n

lemma dvd_trans {a b c : Nat} (h1 : a ∣ b) (h2 : b ∣ c) : a ∣ c := sorry

lemma exists_prime_factor : ∀ (n : Nat), 2 ≤ n →
    ∃ (p : Nat), prime_factor p n := by
  by_strong_induc
  fix n : Nat
  assume ih : ∀ n_1 < n, 2 ≤ n_1 → ∃ (p : Nat), prime_factor p n_1
  assume h1 : 2 ≤ n
  by_cases h2 : prime n
  · -- Case 1. h2 : prime n
    apply Exists.intro n
    define            --Goal : prime n ∧ n ∣ n
    show prime n ∧ n ∣ n from And.intro h2 (dvd_self n)
    done
  · -- Case 2. h2 : ¬prime n
    define at h2
      --h2 : ¬(2 ≤ n ∧ ¬∃ (a b : Nat), a * b = n ∧ a < n ∧ b < n)
    demorgan at h2
    disj_syll h2 h1
    obtain (a : Nat) (h3 : ∃ (b : Nat), a * b = n ∧ a < n ∧ b < n) from h2
    obtain (b : Nat) (h4 : a * b = n ∧ a < n ∧ b < n) from h3
    have h5 : 2 ≤ a := by
      by_contra h6
      have h7 : a ≤ 1 := by linarith
      have h8 : n ≤ b :=
        calc n
          _ = a * b := h4.left.symm
          _ ≤ 1 * b := by rel [h7]
          _ = b := by ring
      linarith        --n ≤ b contradicts b < n
      done
    have h6 : ∃ (p : Nat), prime_factor p a := ih a h4.right.left h5
    obtain (p : Nat) (h7 : prime_factor p a) from h6
    apply Exists.intro p
    define            --Goal : prime p ∧ p ∣ n
    define at h7      --h7 : prime p ∧ p ∣ a
    apply And.intro h7.left
    have h8 : a ∣ n := by
      apply Exists.intro b
      show n = a * b from (h4.left).symm
      done
    show p ∣ n from dvd_trans h7.right h8
    done
  done
```

Of course, by the well-ordering principle, an immediate consequence of this lemma is that every number greater than or equal to 2 has a *smallest* prime factor.

```lean
lemma exists_least_prime_factor {n : Nat} (h : 2 ≤ n) :
    ∃ (p : Nat), prime_factor p n ∧
    ∀ (q : Nat), prime_factor q n → p ≤ q := by
  set S : Set Nat := {p : Nat | prime_factor p n}
  have h2 : ∃ (p : Nat), p ∈ S := exists_prime_factor n h
  show ∃ (p : Nat), prime_factor p n ∧
    ∀ (q : Nat), prime_factor q n → p ≤ q from well_ord_princ S h2
  done
```

To talk about prime factorizations of positive integers, we'll need to introduce a new type.  If `U` is any type, then `List U` is the type of lists of objects of type `U`.  Such a list is written in square brackets, with the entries separated by commas.  For example, `[3, 7, 1]` has type `List Nat`.  The notation `[]` denotes the empty list, and if `a` has type `U` and `l` has type `List U`, then `a :: l` denotes the list consisting of `a` followed by the entries of `l`.  The empty list is sometimes called the `nil` list, and the operation of constructing a list `a :: l` from `a` and `l` is called `cons` (short for *construct*).  Every list can be constructed by applying the `cons` operation repeatedly, starting with the `nil` list.  For example,

::: {.ind}
```
[3, 7, 1] = 3 :: [7, 1] = 3 :: (7 :: [1]) = 3 :: (7 :: (1 :: [])).
```
:::

If `l` has type `List U` and `a` has type `U`, then `a ∈ l` means that `a` is one of the entries in the list `l`.  For example, `7 ∈ [3, 7, 1]`.  Lean knows several theorems about this notation:

::: {.ind}
```
@List.not_mem_nil : ∀ {α : Type u_1} (a : α),
                        a ∉ []

@List.mem_cons : ∀ {α : Type u_1} {a b : α} {l : List α},
                        a ∈ b :: l ↔ a = b ∨ a ∈ l

@List.mem_cons_self : ∀ {α : Type u_1} (a : α) (l : List α),
                        a ∈ a :: l

@List.mem_cons_of_mem : ∀ {α : Type u_1} (y : α) {a : α} {l : List α},
                        a ∈ l → a ∈ y :: l
```
:::

The first two theorems give the conditions under which something is a member of the `nil` list or a list constructed by `cons`, and the last two are easy consequences of the second.

To define prime factorizations, we must define several concepts first.  Some of these concepts are most easily defined recursively.

```lean
def all_prime (l : List Nat) : Prop := ∀ p ∈ l, prime p

def nondec (l : List Nat) : Prop :=
  match l with
    | [] => True   --Of course, True is a proposition that is always true
    | n :: L => (∀ m ∈ L, n ≤ m) ∧ nondec L

def nondec_prime_list (l : List Nat) : Prop := all_prime l ∧ nondec l

def prod (l : List Nat) : Nat :=
  match l with
    | [] => 1
    | n :: L => n * (prod L)

def prime_factorization (n : Nat) (l : List Nat) : Prop :=
  nondec_prime_list l ∧ prod l = n
```

According to these definitions, `all_prime l` means that every member of the list `l` is prime, `nondec l` means that every member of `l` is less than or equal to all later members, `prod l` is the product of all members of `l`, and `prime_factorization n l` means that `l` is a nondecreasing list of prime numbers whose product is `n`.  It will be convenient to spell out some consequences of these definitions in several lemmas:

```lean
lemma all_prime_nil : all_prime [] := by
  define     --Goal : ∀ p ∈ [], prime p
  fix p : Nat
  contrapos  --Goal : ¬prime p → p ∉ []
  assume h1 : ¬prime p
  show p ∉ [] from List.not_mem_nil p
  done

lemma all_prime_cons (n : Nat) (L : List Nat) :
    all_prime (n :: L) ↔ prime n ∧ all_prime L := by
  apply Iff.intro
  · -- (→)
    assume h1 : all_prime (n :: L)  --Goal : prime n ∧ all_prime L
    define at h1  --h1 : ∀ p ∈ n :: L, prime p
    apply And.intro (h1 n (List.mem_cons_self n L))
    define        --Goal : ∀ p ∈ L, prime p
    fix p : Nat
    assume h2 : p ∈ L
    show prime p from h1 p (List.mem_cons_of_mem n h2)
    done
  · -- (←)
    assume h1 : prime n ∧ all_prime L  --Goal : all_prime (n :: l)
    define : all_prime L at h1
    define
    fix p : Nat
    assume h2 : p ∈ n :: L
    rewrite [List.mem_cons] at h2   --h2 : p = n ∨ p ∈ L
    by_cases on h2
    · -- Case 1. h2 : p = n
      rewrite [h2]
      show prime n from h1.left
      done
    · -- Case 2. h2 : p ∈ L
      show prime p from h1.right p h2
      done
    done
  done

lemma nondec_nil : nondec [] := by
  define  --Goal : True
  trivial --trivial proves some obviously true statements, such as True
  done

lemma nondec_cons (n : Nat) (L : List Nat) :
    nondec (n :: L) ↔ (∀ m ∈ L, n ≤ m) ∧ nondec L := by rfl

lemma prod_nil : prod [] = 1 := by rfl

lemma prod_cons : prod (n :: L) = n * (prod L) := by rfl
```

Before we can prove the existence of prime factorizations, we will need one more fact: every member of a list of natural numbers divides the product of the list.  The proof will be by induction on the length of the list, so we will need to know how to work with lengths of lists in Lean.  If `l` is a list, then the length of `l` is `List.length l`, which can also be written more briefly as `l.length`.  We'll need a few more theorems about lists:

::: {.ind}
```
@List.length_eq_zero : ∀ {α : Type u_1} {l : List α},
                      l.length = 0 ↔ l = []

@List.length_cons : ∀ {α : Type u_1} (a : α) (as : List α),
                      (a :: as).length = as.length + 1

@List.exists_cons_of_ne_nil : ∀ {α : Type u_1} {l : List α},
                      l ≠ [] → ∃ (b : α) (L : List α), l = b :: L
```
:::

And we'll need one more lemma, which follows from the three theorems above; we leave the proof as an exercise for you:

```lean
lemma exists_cons_of_length_eq_succ {A : Type}
    {l : List A} {n : Nat} (h : l.length = n + 1) :
    ∃ (a : A) (L : List A), l = a :: L ∧ L.length = n := sorry
```

We can now prove that every member of a list of natural numbers divides the product of the list.  After proving it by induction on the length of the list, we restate the lemma in a more convenient form.

```lean
lemma list_elt_dvd_prod_by_length (a : Nat) : ∀ (n : Nat),
    ∀ (l : List Nat), l.length = n → a ∈ l → a ∣ prod l := by
  by_induc
  · --Base Case
    fix l : List Nat
    assume h1 : l.length = 0
    rewrite [List.length_eq_zero] at h1     --h1 : l = []
    rewrite [h1]                            --Goal : a ∈ [] → a ∣ prod []
    contrapos
    assume h2 : ¬a ∣ prod []
    show a ∉ [] from List.not_mem_nil a
    done
  · -- Induction Step
    fix n : Nat
    assume ih : ∀ (l : List Nat), l.length = n → a ∈ l → a ∣ prod l
    fix l : List Nat
    assume h1 : l.length = n + 1            --Goal : a ∈ l → a ∣ prod l
    obtain (b : Nat) (h2 : ∃ (L : List Nat),
      l = b :: L ∧ L.length = n) from exists_cons_of_length_eq_succ h1
    obtain (L : List Nat) (h3 : l = b :: L ∧ L.length = n) from h2
    have h4 : a ∈ L → a ∣ prod L := ih L h3.right
    assume h5 : a ∈ l
    rewrite [h3.left, prod_cons]            --Goal : a ∣ b * prod L
    rewrite [h3.left, List.mem_cons] at h5  --h5 : a = b ∨ a ∈ L
    by_cases on h5
    · -- Case 1. h5 : a = b
      apply Exists.intro (prod L)
      rewrite [h5]
      rfl
      done
    · -- Case 2. h5 : a ∈ L
      have h6 : a ∣ prod L := h4 h5
      have h7 : prod L ∣ b * prod L := by
        apply Exists.intro b
        ring
        done
      show a ∣ b * prod L from dvd_trans h6 h7
      done
    done
  done

lemma list_elt_dvd_prod {a : Nat} {l : List Nat}
    (h : a ∈ l) : a ∣ prod l := by
  set n : Nat := l.length
  have h1 : l.length = n := by rfl
  show a ∣ prod l from list_elt_dvd_prod_by_length a n l h1 h
  done
```

The proof that every positive integer has a prime factorization is now long but straightforward.

```lean
lemma exists_prime_factorization : ∀ (n : Nat), n ≥ 1 →
    ∃ (l : List Nat), prime_factorization n l := by
  by_strong_induc
  fix n : Nat
  assume ih : ∀ n_1 < n, n_1 ≥ 1 →
    ∃ (l : List Nat), prime_factorization n_1 l
  assume h1 : n ≥ 1
  by_cases h2 : n = 1
  · -- Case 1. h2 : n = 1
    apply Exists.intro []
    define
    apply And.intro
    · -- Proof of nondec_prime_list []
      define
      show all_prime [] ∧ nondec [] from
        And.intro all_prime_nil nondec_nil
      done
    · -- Proof of prod [] = n
      rewrite [prod_nil, h2]
      rfl
      done
    done
  · -- Case 2. h2 : n ≠ 1
    have h3 : n ≥ 2 := lt_of_le_of_ne' h1 h2
    obtain (p : Nat) (h4 : prime_factor p n ∧ ∀ (q : Nat),
      prime_factor q n → p ≤ q) from exists_least_prime_factor h3
    have p_prime_factor : prime_factor p n := h4.left
    define at p_prime_factor
    have p_prime : prime p := p_prime_factor.left
    have p_dvd_n : p ∣ n := p_prime_factor.right
    have p_least : ∀ (q : Nat), prime_factor q n → p ≤ q := h4.right
    obtain (m : Nat) (n_eq_pm : n = p * m) from p_dvd_n
    have h5 : m ≠ 0 := by
      contradict h1 with h6
      have h7 : n = 0 :=
        calc n
          _ = p * m := n_eq_pm
          _ = p * 0 := by rw [h6]
          _ = 0 := by ring
      rewrite [h7]
      decide
      done
    have m_pos : 0 < m := Nat.pos_of_ne_zero h5
    have m_lt_n : m < n := by
      define at p_prime
      show m < n from
        calc m
          _ < m + m := by linarith
          _ = 2 * m := by ring
          _ ≤ p * m := by rel [p_prime.left]
          _ = n := n_eq_pm.symm
      done
    obtain (L : List Nat) (h6 : prime_factorization m L)
      from ih m m_lt_n m_pos
    define at h6
    have ndpl_L : nondec_prime_list L := h6.left
    define at ndpl_L
    apply Exists.intro (p :: L)
    define
    apply And.intro
    · -- Proof of nondec_prime_list (p :: L)
      define
      apply And.intro
      · -- Proof of all_prime (p :: L)
        rewrite [all_prime_cons]
        show prime p ∧ all_prime L from And.intro p_prime ndpl_L.left
        done
      · -- Proof of nondec (p :: L)
        rewrite [nondec_cons]
        apply And.intro _ ndpl_L.right
        fix q : Nat
        assume q_in_L : q ∈ L
        have h7 : q ∣ prod L := list_elt_dvd_prod q_in_L
        rewrite [h6.right] at h7   --h7 : q ∣ m
        have h8 : m ∣ n := by
          apply Exists.intro p
          rewrite [n_eq_pm]
          ring
          done
        have q_dvd_n : q ∣ n := dvd_trans h7 h8
        have ap_L : all_prime L := ndpl_L.left
        define at ap_L
        have q_prime_factor : prime_factor q n :=
          And.intro (ap_L q q_in_L) q_dvd_n
        show p ≤ q from p_least q q_prime_factor
        done
      done
    · -- Proof of prod (p :: L) = n
      rewrite [prod_cons, h6.right, n_eq_pm]
      rfl
      done
    done
  done
```

We now turn to the proof that the prime factorization of a positive integer is unique.  In preparation for that proof, *HTPI* defines two numbers to be *relatively prime* if their greatest common divisor is 1, and then it uses that concept to prove two theorems, 7.2.2 and 7.2.3.  Here are similar proofs of those theorems in Lean, with the proof of one lemma left as an exercise.  In the proof of Theorem 7.2.2, we begin, as we did in the proof of Theorem 7.1.6, by converting the goal from natural numbers to integers so that we can use integer algebra.

```lean
def rel_prime (a b : Nat) : Prop := gcd a b = 1

theorem Theorem_7_2_2 {a b c : Nat}
    (h1 : c ∣ a * b) (h2 : rel_prime a c) : c ∣ b := by
  rewrite [←Int.natCast_dvd_natCast]  --Goal : ↑c ∣ ↑b
  define at h1; define at h2; define
  obtain (j : Nat) (h3 : a * b = c * j) from h1
  set s : Int := gcd_c1 a c
  set t : Int := gcd_c2 a c
  have h4 : s * ↑a + t * ↑c = ↑(gcd a c) := gcd_lin_comb c a
  rewrite [h2, Nat.cast_one] at h4  --h4 : s * ↑a + t * ↑c = (1 : Int)
  apply Exists.intro (s * ↑j + t * ↑b)
  show ↑b = ↑c * (s * ↑j + t * ↑b) from
    calc ↑b
      _ = (1 : Int) * ↑b := (one_mul _).symm
      _ = (s * ↑a + t * ↑c) * ↑b := by rw [h4]
      _ = s * (↑a * ↑b) + t * ↑c * ↑b := by ring
      _ = s * (↑c * ↑j) + t * ↑c * ↑b := by
            rw [←Nat.cast_mul a b, h3, Nat.cast_mul c j]
      _ = ↑c * (s * ↑j + t * ↑b) := by ring
  done

lemma dvd_prime {a p : Nat}
    (h1 : prime p) (h2 : a ∣ p) : a = 1 ∨ a = p := sorry

lemma rel_prime_of_prime_not_dvd {a p : Nat}
    (h1 : prime p) (h2 : ¬p ∣ a) : rel_prime a p := by
  have h3 : gcd a p ∣ a := gcd_dvd_left a p
  have h4 : gcd a p ∣ p := gcd_dvd_right a p
  have h5 : gcd a p = 1 ∨ gcd a p = p := dvd_prime h1 h4
  have h6 : gcd a p ≠ p := by
    contradict h2 with h6
    rewrite [h6] at h3
    show p ∣ a from h3
    done
  disj_syll h5 h6
  show rel_prime a p from h5
  done

theorem Theorem_7_2_3 {a b p : Nat}
    (h1 : prime p) (h2 : p ∣ a * b) : p ∣ a ∨ p ∣ b := by
  or_right with h3
  have h4 : rel_prime a p := rel_prime_of_prime_not_dvd h1 h3
  show p ∣ b from Theorem_7_2_2 h2 h4
  done
```

Theorem 7.2.4 in *HTPI* extends Theorem 7.2.3 to show that if a prime number divides the product of a list of natural numbers, then it divides one of the numbers in the list.  (Theorem 7.2.3 is the case of a list of length two.)  The proof in *HTPI* is by induction on the length of the list, and we could use that method to prove the theorem in Lean.  But look back at our proof of the lemma `list_elt_dvd_prod_by_length`, which also used induction on the length of a list.  In the base case, we ended up proving that the `nil` list has the property stated in the lemma, and in the induction step we proved that if a list `L` has the property, then so does any list of the form `b :: L`.  We could think of this as a kind of "induction on lists."  As we observed earlier, every list can be constructed by starting with the `nil` list and applying `cons` finitely many times.  It follows that if the `nil` list has some property, and applying the `cons` operation to a list with the property produces another list with the property, then all lists have the property.  (In fact, a similar principle was at work in our recursive definitions of `nondec l` and `prod l`.)

Lean has a theorem called `List.rec` that can be used to justify induction on lists.  This is a little more convenient than induction on the length of a list, so we'll use it to prove Theorem 7.2.4.  The proof uses two lemmas, whose proofs we leave as exercises for you.

```lean
lemma eq_one_of_dvd_one {n : Nat} (h : n ∣ 1) : n = 1 := sorry

lemma prime_not_one {p : Nat} (h : prime p) : p ≠ 1 := sorry

theorem Theorem_7_2_4 {p : Nat} (h1 : prime p) :
    ∀ (l : List Nat), p ∣ prod l → ∃ a ∈ l, p ∣ a := by
  apply List.rec
  · -- Base Case.  Goal : p ∣ prod [] → ∃ a ∈ [], p ∣ a
    rewrite [prod_nil]
    assume h2 : p ∣ 1
    show ∃ a ∈ [], p ∣ a from
      absurd (eq_one_of_dvd_one h2) (prime_not_one h1)
    done
  · -- Induction Step
    fix b : Nat
    fix L : List Nat
    assume ih : p ∣ prod L → ∃ a ∈ L, p ∣ a
      --Goal : p ∣ prod (b :: L) → ∃ a ∈ b :: L, p ∣ a
    assume h2 : p ∣ prod (b :: L)
    rewrite [prod_cons] at h2
    have h3 : p ∣ b ∨ p ∣ prod L := Theorem_7_2_3 h1 h2
    by_cases on h3
    · -- Case 1. h3 : p ∣ b
      apply Exists.intro b
      show b ∈ b :: L ∧ p ∣ b from
        And.intro (List.mem_cons_self b L) h3
      done
    · -- Case 2. h3 : p ∣ prod L
      obtain (a : Nat) (h4 : a ∈ L ∧ p ∣ a) from ih h3
      apply Exists.intro a
      show a ∈ b :: L ∧ p ∣ a from
        And.intro (List.mem_cons_of_mem b h4.left) h4.right
      done
    done
  done
```

In Theorem 7.2.4, if all members of the list `l` are prime, then we can conclude not merely that `p` divides some member of `l`, but that `p` is one of the members.

```lean
lemma prime_in_list {p : Nat} {l : List Nat}
    (h1 : prime p) (h2 : all_prime l) (h3 : p ∣ prod l) : p ∈ l := by
  obtain (a : Nat) (h4 : a ∈ l ∧ p ∣ a) from Theorem_7_2_4 h1 l h3
  define at h2
  have h5 : prime a := h2 a h4.left
  have h6 : p = 1 ∨ p = a := dvd_prime h5 h4.right
  disj_syll h6 (prime_not_one h1)
  rewrite [h6]
  show a ∈ l from h4.left
  done
```

The uniqueness of prime factorizations follows from Theorem 7.2.5 of *HTPI*, which says that if two nondecreasing lists of prime numbers have the same product, then the two lists must be the same.  In *HTPI*, a key step in the proof of Theorem 7.2.5 is to show that if two nondecreasing lists of prime numbers have the same product, then the last entry of one list is less than or equal to the last entry of the other.  In Lean, because of the way the `cons` operation works, it is easier to work with the first entries of the lists.

```lean
lemma first_le_first {p q : Nat} {l m : List Nat}
    (h1 : nondec_prime_list (p :: l)) (h2 : nondec_prime_list (q :: m))
    (h3 : prod (p :: l) = prod (q :: m)) : p ≤ q := by
  define at h1; define at h2
  have h4 : q ∣ prod (p :: l) := by
    define
    apply Exists.intro (prod m)
    rewrite [←prod_cons]
    show prod (p :: l) = prod (q :: m) from h3
    done
  have h5 : all_prime (q :: m) := h2.left
  rewrite [all_prime_cons] at h5
  have h6 : q ∈ p :: l := prime_in_list h5.left h1.left h4
  have h7 : nondec (p :: l) := h1.right
  rewrite [nondec_cons] at h7
  rewrite [List.mem_cons] at h6
  by_cases on h6
  · -- Case 1. h6 : q = p
    linarith
    done
  · -- Case 2. h6 : q ∈ l
    have h8 : ∀ m ∈ l, p ≤ m := h7.left
    show p ≤ q from h8 q h6
    done
  done
```

The proof of Theorem 7.2.5 is another proof by induction on lists.  It uses a few more lemmas whose proofs we leave as exercises.

```lean
lemma nondec_prime_list_tail {p : Nat} {l : List Nat}
    (h : nondec_prime_list (p :: l)) : nondec_prime_list l := sorry

lemma cons_prod_not_one {p : Nat} {l : List Nat}
    (h : nondec_prime_list (p :: l)) : prod (p :: l) ≠ 1 := sorry

lemma list_nil_iff_prod_one {l : List Nat} (h : nondec_prime_list l) :
    l = [] ↔ prod l = 1 := sorry

lemma prime_pos {p : Nat} (h : prime p) : p > 0 := sorry

theorem Theorem_7_2_5 : ∀ (l1 l2 : List Nat),
    nondec_prime_list l1 → nondec_prime_list l2 →
    prod l1 = prod l2 → l1 = l2 := by
  apply List.rec
  · -- Base Case.  Goal : ∀ (l2 : List Nat), nondec_prime_list [] →
    -- nondec_prime_list l2 → prod [] = prod l2 → [] = l2
    fix l2 : List Nat
    assume h1 : nondec_prime_list []
    assume h2 : nondec_prime_list l2
    assume h3 : prod [] = prod l2
    rewrite [prod_nil, eq_comm, ←list_nil_iff_prod_one h2] at h3
    show [] = l2 from h3.symm
    done
  · -- Induction Step
    fix p : Nat
    fix L1 : List Nat
    assume ih : ∀ (L2 : List Nat), nondec_prime_list L1 →
      nondec_prime_list L2 → prod L1 = prod L2 → L1 = L2
    -- Goal : ∀ (l2 : List Nat), nondec_prime_list (p :: L1) →
    -- nondec_prime_list l2 → prod (p :: L1) = prod l2 → p :: L1 = l2
    fix l2 : List Nat
    assume h1 : nondec_prime_list (p :: L1)
    assume h2 : nondec_prime_list l2
    assume h3 : prod (p :: L1) = prod l2
    have h4 : ¬prod (p :: L1) = 1 := cons_prod_not_one h1
    rewrite [h3, ←list_nil_iff_prod_one h2] at h4
    obtain (q : Nat) (h5 : ∃ (L : List Nat), l2 = q :: L) from
      List.exists_cons_of_ne_nil h4
    obtain (L2 : List Nat) (h6 : l2 = q :: L2) from h5
    rewrite [h6] at h2    --h2 : nondec_prime_list (q :: L2)
    rewrite [h6] at h3    --h3 : prod (p :: L1) = prod (q :: L2)
    have h7 : p ≤ q := first_le_first h1 h2 h3
    have h8 : q ≤ p := first_le_first h2 h1 h3.symm
    have h9 : p = q := by linarith
    rewrite [h9, prod_cons, prod_cons] at h3
      --h3 : q * prod L1 = q * prod L2
    have h10 : nondec_prime_list L1 := nondec_prime_list_tail h1
    have h11 : nondec_prime_list L2 := nondec_prime_list_tail h2
    define at h2
    have h12 : all_prime (q :: L2) := h2.left
    rewrite [all_prime_cons] at h12
    have h13 : q > 0 := prime_pos h12.left
    have h14 : prod L1 = prod L2 := Nat.eq_of_mul_eq_mul_left h13 h3
    have h15 : L1 = L2 := ih L2 h10 h11 h14
    rewrite [h6, h9, h15]
    rfl
    done
  done
```

Putting it all together, we can finally prove the fundamental theorem of arithmetic, which is stated as Theorem 7.2.6 in *HTPI*:

```lean
theorem fund_thm_arith (n : Nat) (h : n ≥ 1) :
    ∃! (l : List Nat), prime_factorization n l := by
  exists_unique
  · -- Existence
    show ∃ (l : List Nat), prime_factorization n l from
      exists_prime_factorization n h
    done
  · -- Uniqueness
    fix l1 : List Nat; fix l2 : List Nat
    assume h1 : prime_factorization n l1
    assume h2 : prime_factorization n l2
    define at h1; define at h2
    have h3 : prod l1 = n := h1.right
    rewrite [←h2.right] at h3
    show l1 = l2 from Theorem_7_2_5 l1 l2 h1.left h2.left h3
    done
  done
```

### Exercises

::: {.numex arguments="1"}
```lean
lemma dvd_prime {a p : Nat}
    (h1 : prime p) (h2 : a ∣ p) : a = 1 ∨ a = p := sorry
```
:::

::: {.numex arguments="2"}
```lean
--Hints:  Start with apply List.rec.
--You may find the theorem mul_ne_zero useful.
theorem prod_nonzero_nonzero : ∀ (l : List Nat),
    (∀ a ∈ l, a ≠ 0) → prod l ≠ 0 := sorry
```
:::

::: {.numex arguments="3"}
```lean
theorem rel_prime_iff_no_common_factor (a b : Nat) :
    rel_prime a b ↔ ¬∃ (p : Nat), prime p ∧ p ∣ a ∧ p ∣ b := sorry
```
:::

::: {.numex arguments="4"}
```lean
theorem rel_prime_symm {a b : Nat} (h : rel_prime a b) :
    rel_prime b a := sorry
```
:::

::: {.numex arguments="5"}
```lean
lemma in_prime_factorization_iff_prime_factor {a : Nat} {l : List Nat}
    (h1 : prime_factorization a l) (p : Nat) :
    p ∈ l ↔ prime_factor p a := sorry
```
:::

::: {.numex arguments="6"}
```lean
theorem Exercise_7_2_5 {a b : Nat} {l m : List Nat}
    (h1 : prime_factorization a l) (h2 : prime_factorization b m) :
    rel_prime a b ↔ (¬∃ (p : Nat), p ∈ l ∧ p ∈ m) := sorry
```
:::

::: {.numex arguments="7"}
```lean
theorem Exercise_7_2_6 (a b : Nat) :
    rel_prime a b ↔ ∃ (s t : Int), s * a + t * b = 1 := sorry
```
:::

::: {.numex arguments="8"}
```lean
theorem Exercise_7_2_7 {a b a' b' : Nat}
    (h1 : rel_prime a b) (h2 : a' ∣ a) (h3 : b' ∣ b) :
    rel_prime a' b' := sorry
```
:::

::: {.numex arguments="9"}
```lean
theorem Exercise_7_2_9 {a b j k : Nat}
    (h1 : gcd a b ≠ 0) (h2 : a = j * gcd a b) (h3 : b = k * gcd a b) :
    rel_prime j k := sorry
```
:::

::: {.numex arguments="10"}
```lean
theorem Exercise_7_2_17a (a b c : Nat) :
    gcd a (b * c) ∣ gcd a b * gcd a c := sorry
```
:::

## 7.3. Modular Arithmetic

If $m$ is a positive integer and $a$ and $b$ are integers, then *HTPI* uses the notation $a \equiv b\pmod m$, or sometimes $a \equiv_m b$, to indicate that $a$ is congruent to $b$ modulo $m$, which is defined to mean $m \mid (a - b)$.  Congruence modulo $m$ is an equivalence relation on the integers, and therefore it induces a partition $\mathbb{Z}/{\equiv_m}$ of the integers, as shown in Section 4.5 of *HTPI*.  The elements of this partition are the equivalence classes $[a]_m$ for $a \in \mathbb{Z}$; we will call these *congruence classes modulo $m$*.  Section 7.3 of *HTPI* defines operations of addition and multiplication of congruence classes and proves algebraic properties of those operations.

For the purpose of working out the rules of modular arithmetic, the only important properties of congruence classes are the following:

1.  For every integer $a$, there is a corresponding congruence class $[a]_m \in \mathbb{Z}/{\equiv_m}$.
2.  For every congruence class $X \in \mathbb{Z}/{\equiv_m}$, there is some integer $a$ such that $X = [a]_m$.
3.  For all integers $a$ and $b$, $[a]_m = [b]_m$ if and only if $a \equiv_m b$.
4.  For all integers $a$ and $b$, $[a]_m + [b]_m = [a + b]_m$.
5.  For all integers $a$ and $b$, $[a]_m \cdot [b]_m = [ab]_m$.

To study congruence modulo `m` in Lean, we will declare `m` to have type `Nat`, which allows for the possibility that `m = 0`, but we will mostly focus on the case `m ≠ 0`.  For `a` and `b` of type `Int`, we define `congr_mod m a b` to mean that `a` is congruent to `b` modulo `m`.  Notice that to define this relation in Lean, we must coerce `m` to be an integer so that we can use it in the divisibility relation on the integers.

```lean
def congr_mod (m : Nat) (a b : Int) : Prop := (↑m : Int) ∣ (a - b)
```

We can teach Lean to use more familiar notation for congruence modulo `m` by giving the following command:

```lean
notation:50 a " ≡ " b " (MOD " m ")" => congr_mod m a b
```

This tells Lean that if we type `a ≡ b (MOD m)`, then Lean should interpret it as `congr_mod m a b`.  (To enter the symbol `≡`, type `\==`.  Don't worry about the `:50` in the `notation` command above.  It is there to help Lean parse this new notation when it occurs together with other notation.)

We can now prove that congruence modulo `m` is reflexive, symmetric, and transitive.  In these proofs, we leave it to Lean to fill in coercions when they are necessary, and as usual, we leave some details as exercises.

```lean
theorem congr_refl (m : Nat) : ∀ (a : Int), a ≡ a (MOD m) := sorry

theorem congr_symm {m : Nat} : ∀ {a b : Int},
    a ≡ b (MOD m) → b ≡ a (MOD m) := by
  fix a : Int; fix b : Int
  assume h1 : a ≡ b (MOD m)
  define at h1                 --h1 : ∃ (c : Int), a - b = ↑m * c
  define                       --Goal : ∃ (c : Int), b - a = ↑m * c
  obtain (c : Int) (h2 : a - b = m * c) from h1
  apply Exists.intro (-c)
  show b - a = m * (-c) from
    calc b - a
      _ = -(a - b) := by ring
      _ = -(m * c) := by rw [h2]
      _ = m * (-c) := by ring
  done

theorem congr_trans {m : Nat} : ∀ {a b c : Int},
    a ≡ b (MOD m) → b ≡ c (MOD m) → a ≡ c (MOD m) := sorry
```

We could now repeat the entire development of $\mathbb{Z}/{\equiv_m}$ in Lean, but there is no need to do so; such a development is already included in Lean's library of definitions and theorems.  For each natural number `m`, Lean has a type `ZMod m`, and the objects of that type are Lean's version of the congruence classes modulo `m`.  We should warn you that Lean's way of defining `ZMod m` differs in some ways from *HTPI*'s definition of $\mathbb{Z}/{\equiv_m}$.  In particular, objects of type `ZMod m` are not sets of integers.  Thus, if `X` has type `ZMod m` and `a` has type `Int`, then Lean will not understand what you mean if you write `a ∈ X`.  However, Lean's congruence classes have the properties 1--5 listed above, and that's all that will matter to us.

Property 1 says that if `a` has type `Int`, then there should be a corresponding congruence class in `ZMod m`.  In fact, you can find the corresponding congruence class by simply coercing `a` to have type `ZMod m`.  But for the sake of clarity, we will introduce a function for computing the congruence class modulo `m` of `a`:

```lean
def cc (m : Nat) (a : Int) : ZMod m := (↑a : ZMod m)
```

Thus, `cc m a` is the congruence class modulo `m` of `a`.  Once again, it will be convenient to teach Lean to use more familiar notation for congruence classes, so we give the command:

```lean
notation:max "["a"]_"m:max => cc m a
```

Now if we type `[a]_m`, then Lean will interpret it as `cc m a`.  Thus, from now on, `[a]_m` will be our notation in Lean for the congruence class modulo `m` of `a`; it corresponds to the *HTPI* notation $[a]_m$.  (Once again, you can ignore the two occurrences of `:max` in the `notation` command above.)

Properties 2--5 of congruence classes are established by the following theorems:

```lean
theorem cc_rep {m : Nat} (X : ZMod m) : ∃ (a : Int), X = [a]_m

theorem cc_eq_iff_congr (m : Nat) (a b : Int) :
    [a]_m = [b]_m ↔ a ≡ b (MOD m)

theorem add_class (m : Nat) (a b : Int) :
    [a]_m + [b]_m = [a + b]_m

theorem mul_class (m : Nat) (a b : Int) :
    [a]_m * [b]_m = [a * b]_m
```

We won't discuss the proofs of these theorems, since they depend on details of Lean's representation of objects of type `ZMod m` that are beyond the scope of this book.  But these theorems are all we will need to use to develop the theory of modular arithmetic.

In many of our theorems about `ZMod m`, we will need to include a hypothesis that `m ≠ 0`.  We will usually state this hypothesis in the form `NeZero m`, which is a proposition that is equivalent to `m ≠ 0`.  Indeed, there is a theorem in Lean's library that asserts this equivalence:

::: {.ind}
```
@neZero_iff : ∀ {R : Type u_1} [inst : Zero R] {n : R},
              NeZero n ↔ n ≠ 0
```
:::

What distinguishes `NeZero m` from `m ≠ 0` is that `NeZero m` is what is called a *type class*.  What this means is that, once Lean has a proof of `NeZero m` for some natural number `m`, it will remember that proof and be able to recall it when necessary.  As a result, `NeZero m` can be used as a new kind of implicit argument in the statement of a theorem.  To make it an implicit argument, we write it in square brackets, like this: `[NeZero m]`.  When applying a theorem that includes this hypothesis, there is no need to supply a proof that `m ≠ 0`; as long as Lean knows about such a proof, it will recall that proof on its own.  When you are proving a theorem that includes the hypothesis `[NeZero m]`, Lean will recognize `NeZero.ne m` as a proof that `m ≠ 0`.

The first theorem in Section 7.3 of *HTPI*, Theorem 7.3.1, says that if `m ≠ 0`, then every integer `a` is congruent modulo `m` to exactly one integer `r` satisfying `0 ≤ r < m`.  As explained in *HTPI*, we say that `{0, 1, ..., m - 1}` is a *complete residue system modulo `m`*.  This implies that the objects of type `ZMod m` are precisely the congruence classes `[0]_m`, `[1]_m`, ..., `[m - 1]_m`.  

The proof of Theorem 7.3.1 makes use of the quotient and remainder when `a` is divided by `m`.  In Section 6.4, we learned about the Lean theorems `Nat.div_add_mod` and `Nat.mod_lt`, but those theorems concerned quotients and remainders when dividing *natural numbers*.  Fortunately, Lean has similar theorems for dealing with division of integers:

::: {.ind}
```
Int.ediv_add_emod : ∀ (a b : ℤ), b * (a / b) + a % b = a

Int.emod_lt_of_pos : ∀ (a : ℤ) {b : ℤ}, 0 < b → a % b < b

Int.emod_nonneg : ∀ (a : ℤ) {b : ℤ}, b ≠ 0 → 0 ≤ a % b
```
:::

We now have all the background we need to prove Theorem 7.3.1 in Lean.  We begin with a few lemmas, some of which require the hypothesis `[NeZero m]`.  The proof of the theorem closely follows the proof in *HTPI*.  Note that all of the proofs below involve the expression `a % m`.  Since `a` is an integer, the operator `%` in this expression must be the integer version of the mod operator, and therefore `m` must be coerced to be an integer.  Thus, Lean interprets `a % m` as `a % ↑m`

```lean
lemma mod_nonneg (m : Nat) [NeZero m] (a : Int) : 0 ≤ a % m := by
  have h1 : (↑m : Int) ≠ 0 := (Nat.cast_ne_zero).rtl (NeZero.ne m)
  show 0 ≤ a % m from Int.emod_nonneg a h1
  done

lemma mod_lt (m : Nat) [NeZero m] (a : Int) : a % m < m := sorry

lemma congr_mod_mod (m : Nat) (a : Int) : a ≡ a % m (MOD m) := by
  define
  have h1 : m * (a / m) + a % m = a := Int.ediv_add_emod a m
  apply Exists.intro (a / m)
  show a - a % m = m * (a / m) from
    calc a - (a % m)
      _ = m * (a / m) + a % m - a % m := by rw [h1]
      _ = m * (a / m) := by ring
  done

lemma mod_cmpl_res (m : Nat) [NeZero m] (a : Int) :
    0 ≤ a % m ∧ a % m < m ∧ a ≡ a % m (MOD m) :=
  And.intro (mod_nonneg m a) (And.intro (mod_lt m a) (congr_mod_mod m a))

theorem Theorem_7_3_1 (m : Nat) [NeZero m] (a : Int) :
    ∃! (r : Int), 0 ≤ r ∧ r < m ∧ a ≡ r (MOD m) := by
  exists_unique
  · -- Existence
    apply Exists.intro (a % m)
    show 0 ≤ a % m ∧ a % m < m ∧ a ≡ a % m (MOD m)
      from mod_cmpl_res m a
    done
  · -- Uniqueness
    fix r1 : Int; fix r2 : Int
    assume h1 : 0 ≤ r1 ∧ r1 < m ∧ a ≡ r1 (MOD m)
    assume h2 : 0 ≤ r2 ∧ r2 < m ∧ a ≡ r2 (MOD m)
    have h3 : r1 ≡ r2 (MOD m) :=
      congr_trans (congr_symm h1.right.right) h2.right.right
    obtain (d : Int) (h4 : r1 - r2 = m * d) from h3
    have h5 : r1 - r2 < m * 1 := by linarith
    have h6 : m * (-1) < r1 - r2 := by linarith
    rewrite [h4] at h5   --h5 : m * d < m * 1
    rewrite [h4] at h6   --h6 : m * -1 < m * d
    have h7 : (↑m : Int) ≥ 0 := Nat.cast_nonneg m
    have h8 : d < 1 := lt_of_mul_lt_mul_of_nonneg_left h5 h7
    have h9 : -1 < d := lt_of_mul_lt_mul_of_nonneg_left h6 h7
    have h10 : d = 0 := by linarith
    show r1 = r2 from
      calc r1
        _ = r1 - r2 + r2 := by ring
        _ = m * 0 + r2 := by rw [h4, h10]
        _ = r2 := by ring
    done
  done
```

The lemma `mod_cmpl_res` above says that `a % m` is an element of the complete residue system `{0, 1, ..., m - 1}` that is congruent to `a` modulo `m`.  The lemma requires the hypothesis `[NeZero m]`, because its proof appeals to two previous lemmas, `mod_nonneg` and `mod_lt`, that require that hypothesis.  But when the proof invokes those previous lemmas, this hypothesis is not mentioned, because it is an implicit argument.

An immediate consequence of the lemma `congr_mod_mod` is the following lemma, which will be useful to us later.

```lean
lemma cc_eq_mod (m : Nat) (a : Int) : [a]_m = [a % m]_m := 
  (cc_eq_iff_congr m a (a % m)).rtl (congr_mod_mod m a)
```

Theorem 7.3.6 in *HTPI* states a number of algebraic properties of modular arithmetic.  These properties all follow easily from the theorems we have already stated.  To illustrate this, we prove two parts of the theorem.

```lean
theorem Theorem_7_3_6_1 {m : Nat} (X Y : ZMod m) : X + Y = Y + X := by
  obtain (a : Int) (h1 : X = [a]_m) from cc_rep X
  obtain (b : Int) (h2 : Y = [b]_m) from cc_rep Y
  rewrite [h1, h2]
  have h3 : a + b = b + a := by ring
  show [a]_m + [b]_m = [b]_m + [a]_m from
    calc [a]_m + [b]_m
      _ = [a + b]_m := add_class m a b
      _ = [b + a]_m := by rw [h3]
      _ = [b]_m + [a]_m := (add_class m b a).symm
  done

theorem Theorem_7_3_6_7 {m : Nat} (X : ZMod m) : X * [1]_m = X := by
  obtain (a : Int) (h1 : X = [a]_m) from cc_rep X
  rewrite [h1]
  have h2 : a * 1 = a := by ring
  show [a]_m * [1]_m = [a]_m from
    calc [a]_m * [1]_m
      _ = [a * 1]_m := mul_class m a 1
      _ = [a]_m := by rw [h2]
  done
```

`Theorem_7_3_6_7` shows that `[1]_m` is the multiplicative identity element for `ZMod m`.  We say that a congruence class `Y` is a *multiplicative inverse* of another class `X` if `X * Y = [1]_m`, and a congruence class is *invertible* if it has a multiplicative inverse:

```lean
def invertible {m : Nat} (X : ZMod m) : Prop :=
  ∃ (Y : ZMod m), X * Y = [1]_m
```

Which congruence classes are invertible?  The answer is given by Theorem 7.3.7 in *HTPI*, which says that if $a$ is a positive integer, then $[a]_m$ is invertible if and only if $m$ and $a$ are relatively prime.  The proof uses an exercise from the last section.  Here is the Lean version of the proof.

```lean
theorem Exercise_7_2_6 (a b : Nat) :
    rel_prime a b ↔ ∃ (s t : Int), s * a + t * b = 1 := sorry

lemma gcd_c2_inv {m a : Nat} (h1 : rel_prime m a) :
    [a]_m * [gcd_c2 m a]_m = [1]_m := by
  set s : Int := gcd_c1 m a
  have h2 : s * m + (gcd_c2 m a) * a = gcd m a := gcd_lin_comb a m
  define at h1
  rewrite [h1, Nat.cast_one] at h2  --h2 : s * ↑m + gcd_c2 m a * ↑a = 1
  rewrite [mul_class, cc_eq_iff_congr]
  define     --Goal : ∃ (c : Int), ↑a * gcd_c2 m a - 1 = ↑m * c
  apply Exists.intro (-s)
  show a * (gcd_c2 m a) - 1 = m * (-s) from
    calc a * (gcd_c2 m a) - 1
      _ = s * m + (gcd_c2 m a) * a + m * (-s) - 1 := by ring
      _ = 1 + m * (-s) - 1 := by rw [h2]
      _ = m * (-s) := by ring
  done

theorem Theorem_7_3_7 (m a : Nat) :
    invertible [a]_m ↔ rel_prime m a := by
  apply Iff.intro
  · -- (→)
    assume h1 : invertible [a]_m
    define at h1
    obtain (Y : ZMod m) (h2 : [a]_m * Y = [1]_m) from h1
    obtain (b : Int) (h3 : Y = [b]_m) from cc_rep Y
    rewrite [h3, mul_class, cc_eq_iff_congr] at h2
    define at h2
    obtain (c : Int) (h4 : a * b - 1 = m * c) from h2
    rewrite [Exercise_7_2_6]
      --Goal : ∃ (s t : Int), s * ↑m + t * ↑a = 1
    apply Exists.intro (-c)
    apply Exists.intro b
    show (-c) * m + b * a = 1 from
      calc (-c) * m + b * a
        _ = (-c) * m + (a * b - 1) + 1 := by ring
        _ = (-c) * m + m * c + 1 := by rw [h4]
        _ = 1 := by ring
    done
  · -- (←)
    assume h1 : rel_prime m a
    define
    show ∃ (Y : ZMod m), [a]_m * Y = [1]_m from
      Exists.intro [gcd_c2 m a]_m (gcd_c2_inv h1)
    done
  done
```

### Exercises

::: {.numex arguments="1"}
```lean
theorem congr_trans {m : Nat} : ∀ {a b c : Int},
    a ≡ b (MOD m) → b ≡ c (MOD m) → a ≡ c (MOD m) := sorry
```
:::

::: {.numex arguments="2"}
```lean
theorem Theorem_7_3_6_3 {m : Nat} (X : ZMod m) : X + [0]_m = X := sorry
```
:::

::: {.numex arguments="3"}
```lean
theorem Theorem_7_3_6_4 {m : Nat} (X : ZMod m) :
    ∃ (Y : ZMod m), X + Y = [0]_m := sorry
```
:::

::: {.numex arguments="4"}
```lean
theorem Exercise_7_3_4a {m : Nat} (Z1 Z2 : ZMod m)
    (h1 : ∀ (X : ZMod m), X + Z1 = X)
    (h2 : ∀ (X : ZMod m), X + Z2 = X) : Z1 = Z2 := sorry
```
:::

::: {.numex arguments="5"}
```lean
theorem Exercise_7_3_4b {m : Nat} (X Y1 Y2 : ZMod m)
    (h1 : X + Y1 = [0]_m) (h2 : X + Y2 = [0]_m) : Y1 = Y2 := sorry
```
:::

::: {.numex arguments="6"}
```lean
theorem Theorem_7_3_10 (m a : Nat) (b : Int) :
    ¬(↑(gcd m a) : Int) ∣ b → ¬∃ (x : Int), a * x ≡ b (MOD m) := sorry
```
:::

::: {.numex arguments="7"}
```lean
theorem Theorem_7_3_11 (m n : Nat) (a b : Int) (h1 : n ≠ 0) :
    n * a ≡ n * b (MOD n * m) ↔ a ≡ b (MOD m) := sorry
```
:::

::: {.numex arguments="8"}
```lean
theorem Exercise_7_3_16 {m : Nat} {a b : Int} (h : a ≡ b (MOD m)) :
    ∀ (n : Nat), a ^ n ≡ b ^ n (MOD m) := sorry
```
:::

::: {.numex arguments="9"}
```lean
example {m : Nat} [NeZero m] (X : ZMod m) :
    ∃! (a : Int), 0 ≤ a ∧ a < m ∧ X = [a]_m := sorry
```
:::

::: {.numex arguments="10"}
```lean
theorem congr_rel_prime {m a b : Nat} (h1 : a ≡ b (MOD m)) :
    rel_prime m a ↔ rel_prime m b := sorry
```
:::

::: {.numex arguments="11"}
```lean
--Hint: You may find the theorem Int.ofNat_mod_ofNat useful.
theorem rel_prime_mod (m a : Nat) :
    rel_prime m (a % m) ↔ rel_prime m a := sorry
```
:::

::: {.numex arguments="12"}
```lean
lemma congr_iff_mod_eq_Int (m : Nat) (a b : Int) [NeZero m] :
    a ≡ b (MOD m) ↔ a % ↑m = b % ↑m := sorry

--Hint for next theorem: Use the lemma above,
--together with the theorems Int.ofNat_mod_ofNat and Nat.cast_inj.
theorem congr_iff_mod_eq_Nat (m a b : Nat) [NeZero m] :
    ↑a ≡ ↑b (MOD m) ↔ a % m = b % m := sorry
```
:::

## 7.4. Euler's Theorem

The main result of Section 7.4 of *HTPI* is Euler's theorem.  The statement of the theorem involves Euler's totient function $\varphi$.  For any positive integer $m$, *HTPI* defines $\varphi(m)$ to be the number of elements of $\mathbb{Z}/{\equiv_m}$ that have multiplicative inverses.  In order to state and prove Euler's theorem in Lean, our first task is to define a Lean function `phi : Nat → Nat` that computes the totient function.

Since `{0, 1, ..., m - 1}` is a complete residue system modulo `m`, `phi m` can be described as the number of natural numbers `a < m` such that `[a]_m` is invertible.  According to `Theorem_7_3_7`, `[a]_m` is invertible if and only if `m` and `a` are relatively prime, so `phi m` is also equal to the number of natural numbers `a < m` that are relatively prime to `m`.  We begin by defining a function `num_rp_below m k` that counts the number of natural numbers less than `k` that are relatively prime to `m`.

```lean
def num_rp_below (m k : Nat) : Nat :=
  match k with
    | 0 => 0
    | j + 1 => if gcd m j = 1 then (num_rp_below m j) + 1
                else num_rp_below m j
```

This is the first time we have used an `if ... then ... else` expression in a Lean definition.  To prove theorems about such expressions, we will need two theorems from Lean's library, `if_pos` and `if_neg`.  The `#check` command tells us what they say:

::: {.ind}
```
@if_pos : ∀ {c : Prop} {h : Decidable c},
          c → ∀ {α : Sort u_1} {t e : α}, (if c then t else e) = t
          
@if_neg : ∀ {c : Prop} {h : Decidable c},
          ¬c → ∀ {α : Sort u_1} {t e : α}, (if c then t else e) = e
```
:::

Ignoring the implicit arguments, this tells us that if `h` is a proof of a proposition `c`, then `if_pos h` is a proof of `(if c then t else e) = t`, and if `h` is a proof of `¬c`, then `if_neg h` is a proof of `(if c then t else e) = e`.  (Technically, the implicit arguments say that `c` must be a "decidable" proposition, but we won't worry about that detail.)  We often use these theorems with the `rewrite` tactic to rewrite an expression of the form `if c then t else e` as either `t` or `e`, depending on whether `c` is true or false.

```lean
lemma num_rp_below_base {m : Nat} :
    num_rp_below m 0 = 0 := by rfl

lemma num_rp_below_step_rp {m j : Nat} (h : rel_prime m j) :
    num_rp_below m (j + 1) = (num_rp_below m j) + 1 := by
  have h1 : num_rp_below m (j + 1) =
    if gcd m j = 1 then (num_rp_below m j) + 1
    else num_rp_below m j := by rfl
  define at h     --h : gcd m j = 1
  rewrite [if_pos h] at h1
                  --h1 : num_rp_below m (j + 1) = num_rp_below m j + 1
  show num_rp_below m (j + 1) = num_rp_below m j + 1 from h1
  done

lemma num_rp_below_step_not_rp {m j : Nat} (h : ¬rel_prime m j) :
    num_rp_below m (j + 1) = num_rp_below m j := by
  have h1 : num_rp_below m (j +1) =
    if gcd m j = 1 then (num_rp_below m j) + 1
    else num_rp_below m j := by rfl
  define at h     --h : ¬gcd m j = 1
  rewrite [if_neg h] at h1
                  --h1 : num_rp_below m (j + 1) = num_rp_below m j
  show num_rp_below m (j + 1) = num_rp_below m j from h1
  done
```

We can now use `num_rp_below` to define the totient function.

```lean
def phi (m : Nat) : Nat := num_rp_below m m

lemma phi_def (m : Nat) : phi m = num_rp_below m m := by rfl

#eval phi 10   --Answer: 4
```

With this preparation, we can now state the theorem we will prove:

```lean
theorem Theorem_7_4_2 {m a : Nat} [NeZero m] (h1 : rel_prime m a) :
    [a]_m ^ (phi m) = [1]_m
```

In preparation for proving this theorem, *HTPI* first shows that the set of invertible congruence classes is closed under inverses and multiplication.  For our purposes, we will find it useful to prove a slightly different lemma.  Note that Lean knows all of the basic algebraic laws of addition and multiplication of congruence classes, and as a result the `ring` tactic can be used to do algebraic reasoning in `ZMod m`, as illustrated in the proof below.

```lean
lemma prod_inv_iff_inv {m : Nat} {X : ZMod m}
    (h1 : invertible X) (Y : ZMod m) :
    invertible (X * Y) ↔ invertible Y := by
  apply Iff.intro
  · -- (→)
    assume h2 : invertible (X * Y)
    obtain (Z : ZMod m) (h3 : X * Y * Z = [1]_m) from h2
    apply Exists.intro (X * Z)
    rewrite [←h3]  --Goal : Y * (X * Z) = X * Y * Z
    ring     --Note that ring can do algebra in ZMod m
    done
  · -- (←)
    assume h2 : invertible Y
    obtain (Xi : ZMod m) (h3 : X * Xi = [1]_m) from h1
    obtain (Yi : ZMod m) (h4 : Y * Yi = [1]_m) from h2
    apply Exists.intro (Xi * Yi)
    show (X * Y) * (Xi * Yi) = [1]_m from
      calc X * Y * (Xi * Yi)
        _ = (X * Xi) * (Y * Yi) := by ring
        _ = [1]_m * [1]_m := by rw [h3, h4]
        _ = [1]_m := Theorem_7_3_6_7 [1]_m
    done
  done
```

One of the key ideas in the proof of Theorem 7.4.2 in *HTPI* involves computing the product of all invertible congruence classes.  To compute this product in Lean, we begin by defining a function `F m : Nat → ZMod m` as follows:

```lean
def F (m i : Nat) : ZMod m := if gcd m i = 1 then [i]_m else [1]_m

lemma F_rp_def {m i : Nat} (h : rel_prime m i) :
    F m i = [i]_m := by
  have h1 : F m i = if gcd m i = 1 then [i]_m else [1]_m := by rfl
  define at h      --h : gcd m i = 1
  rewrite [if_pos h] at h1
  show F m i = [i]_m from h1
  done

lemma F_not_rp_def {m i : Nat} (h : ¬rel_prime m i) :
    F m i = [1]_m := sorry
```

Note that `F` is defined as a function of two natural numbers, `m` and `i`, but as we discussed in Section 5.4, it follows that the partial application `F m` is a function from `Nat` to `ZMod m`.

Now consider the product `(F m 0) * (F m 1) * ... * (F m (m - 1))`; we will call this the *`F`-product*.  If `m` and `i` are not relatively prime, then `F m i = [1]_m`, and since `[1]_m` is the multiplicative identity element of `ZMod m`, the factor `F m i` contributes nothing to the product.  Thus, the `F`-product is equal to the product of the factors `F m i` for which `m` and `i` are relatively prime.  But for those values of `i`, `F m i = [i]_m`, so the product is equal to the product of all congruence classes `[i]_m` with `m` and `i` relatively prime.  By `Theorem_7_3_7`, that is the product of all invertible congruence classes.

To express the `F`-product in Lean, we imitate our approach to summations, as described in Chapter 6.  We begin by defining `prod_seq j k f` to be the product of a sequence of `j` consecutive values of the function `f`, starting with `f k`:

```lean
def prod_seq {m : Nat}
    (j k : Nat) (f : Nat → ZMod m) : ZMod m :=
  match j with
    | 0 => [1]_m
    | n + 1 => prod_seq n k f * f (k + n)

lemma prod_seq_base {m : Nat}
    (k : Nat) (f : Nat → ZMod m) : prod_seq 0 k f = [1]_m := by rfl

lemma prod_seq_step {m : Nat}
    (n k : Nat) (f : Nat → ZMod m) :
    prod_seq (n + 1) k f = prod_seq n k f * f (k + n) := by rfl

lemma prod_seq_zero_step {m : Nat}
    (n : Nat) (f : Nat → ZMod m) :
    prod_seq (n + 1) 0 f = prod_seq n 0 f * f n := sorry
```

Using this notation, the expression `prod_seq m 0 (F m)` denotes the `F`-product, which, as we saw earlier, is equal to the product of the invertible congruence classes.

Now suppose `a` is a natural number that is relatively prime to `m`.  The next step in the proof in *HTPI* is to multiply each factor in the product of the invertible congruence classes by `[a]_m`.  To do this, we define a function `G` as follows:

```lean
def G (m a i : Nat) : Nat := (a * i) % m
```

Consider the following product, which we will call the *`FG`-product*:

::: {.ind}
```
(F m (G m a 0)) * (F m (G m a 1)) * ... * (F m (G m a (m - 1))).
```
:::

Using the partial application `G m a`, which is a function from `Nat` to `Nat`, we can express this in Lean as `prod_seq m 0 ((F m) ∘ (G m a))`.  To understand this product we will need two facts about `G`.  

```lean
lemma cc_G (m a i : Nat) : [G m a i]_m = [a]_m * [i]_m :=
  calc [G m a i]_m
    _ = [(a * i) % m]_m := by rfl
    _ = [a * i]_m := (cc_eq_mod m (a * i)).symm
    _ = [a]_m * [i]_m := (mul_class m a i).symm

lemma G_rp_iff {m a : Nat} (h1 : rel_prime m a) (i : Nat) :
    rel_prime m (G m a i) ↔ rel_prime m i := by
  have h2 : invertible [a]_m := (Theorem_7_3_7 m a).rtl h1
  show rel_prime m (G m a i) ↔ rel_prime m i from
    calc rel_prime m (G m a i)
      _ ↔ invertible [G m a i]_m := (Theorem_7_3_7 m (G m a i)).symm
      _ ↔ invertible ([a]_m * [i]_m) := by rw [cc_G]
      _ ↔ invertible [i]_m := prod_inv_iff_inv h2 ([i]_m)
      _ ↔ rel_prime m i := Theorem_7_3_7 m i
  done
```

Now let's analyze the `FG`-product.  If `i` is not relatively prime to `m`, then by `G_rp_iff`, `G m a i` is also not relatively prime to `m`, so `F m (G m a i) = [1]_m`.  As before, this means that these terms contribute nothing to the `FG`-product.  If `i` is relatively prime to `m`, then so is `G m a i`, and therefore, by `cc_G`,

::: {.ind}
```
F m (G m a i) = [G m a i]_m = [a]_m * [i]_m = [a]_m * (F m i).
```
:::

This means that, in the `FG`-product, each factor contributed by a value of `i` that is relatively prime to `m` is `[a]_m` times the corresponding factor in the `F`-product.  Since the number of such factors is `phi m`, it follows that the `FG`-product is `[a]_m ^ (phi m)` times the `F`-product.

Let's see if we can prove this in Lean.

```lean
lemma FG_rp {m a i : Nat} (h1 : rel_prime m a) (h2 : rel_prime m i) :
    F m (G m a i) = [a]_m * F m i := by
  have h3 : rel_prime m (G m a i) := (G_rp_iff h1 i).rtl h2
  show F m (G m a i) = [a]_m * F m i from
    calc F m (G m a i)
      _ = [G m a i]_m := F_rp_def h3
      _ = [a]_m * [i]_m := cc_G m a i
      _ = [a]_m * F m i := by rw [F_rp_def h2]
  done

lemma FG_not_rp {m a i : Nat} (h1 : rel_prime m a) (h2 : ¬rel_prime m i) :
    F m (G m a i) = [1]_m := sorry

lemma FG_prod {m a : Nat} (h1 : rel_prime m a) :
    ∀ (k : Nat), prod_seq k 0 ((F m) ∘ (G m a)) =
      [a]_m ^ (num_rp_below m k) * prod_seq k 0 (F m) := by
  by_induc
  · -- Base Case
    show prod_seq 0 0 ((F m) ∘ (G m a)) =
          [a]_m ^ (num_rp_below m 0) * prod_seq 0 0 (F m) from
      calc prod_seq 0 0 ((F m) ∘ (G m a))
        _ = [1]_m := prod_seq_base _ _
        _ = [a]_m ^ 0 * [1]_m := by ring
        _ = [a]_m ^ (num_rp_below m 0) * prod_seq 0 0 (F m) := by
              rw [num_rp_below_base, prod_seq_base]
    done
  · -- Induction Step
    fix k : Nat
    assume ih : prod_seq k 0 ((F m) ∘ (G m a)) =
      [a]_m ^ (num_rp_below m k) * prod_seq k 0 (F m)
    by_cases h2 : rel_prime m k
    · -- Case 1. h2 : rel_prime m k
      show prod_seq (k + 1) 0 ((F m) ∘ (G m a)) =
          [a]_m ^ (num_rp_below m (k + 1)) *
          prod_seq (k + 1) 0 (F m) from
        calc prod_seq (k + 1) 0 ((F m) ∘ (G m a))
          _ = prod_seq k 0 ((F m) ∘ (G m a)) *
              F m (G m a k) := prod_seq_zero_step _ _
          _ = [a]_m ^ (num_rp_below m k) * prod_seq k 0 (F m) *
              F m (G m a k) := by rw [ih]
          _ = [a]_m ^ (num_rp_below m k) * prod_seq k 0 (F m) *
              ([a]_m * F m k) := by rw [FG_rp h1 h2]
          _ = [a]_m ^ ((num_rp_below m k) + 1) *
              ((prod_seq k 0 (F m)) * F m k) := by ring
          _ = [a]_m ^ (num_rp_below m (k + 1)) *
              prod_seq (k + 1) 0 (F m) := by
                rw [num_rp_below_step_rp h2, prod_seq_zero_step]
      done
    · -- Case 2. h2 : ¬rel_prime m k
      show prod_seq (k + 1) 0 ((F m) ∘ (G m a)) =
          [a]_m ^ (num_rp_below m (k + 1)) *
          prod_seq (k + 1) 0 (F m) from
        calc prod_seq (k + 1) 0 ((F m) ∘ (G m a))
          _ = prod_seq k 0 ((F m) ∘ (G m a)) *
              F m (G m a k) := prod_seq_zero_step _ _
          _ = [a]_m ^ (num_rp_below m k) * prod_seq k 0 (F m) *
              F m (G m a k) := by rw [ih]
          _ = [a]_m ^ (num_rp_below m k) * prod_seq k 0 (F m) *
              ([1]_m) := by rw [FG_not_rp h1 h2]
          _ = [a]_m ^ (num_rp_below m k) *
              (prod_seq k 0 (F m) * ([1]_m)) := by ring
          _ = [a]_m ^ (num_rp_below m (k + 1)) *
              prod_seq (k + 1) 0 (F m) := by
                rw [num_rp_below_step_not_rp h2, prod_seq_zero_step,
                F_not_rp_def h2]
      done
    done
  done
```

The lemma `FG_prod`, in the case `k = m`, tells us that

::: {.ind}
```
prod_seq m 0 ((F m) ∘ (G m a)) = [a]_m ^ (phi m) * prod_seq m 0 (F m).
```
:::

In other words, we have proven that the `FG`-product is `[a]_m ^ (phi m)` times the `F`-product.

And now we come to the central idea in the proof of `Theorem_7_4_2`: the congruence classes that are multiplied in the `FG`-product are exactly the same as the congruence classes multiplied in the `F`-product, but listed in a different order.  The reason for this is that the function `G m a` permutes the natural numbers less than `m`.  Since multiplication of congruence classes is commutative and associative, it follows that the `FG`-product and the `F`-product are equal.

To prove these claims, we first define what it means for a function to permute the natural numbers less than a natural number `n`.

```lean
def maps_below (n : Nat) (g : Nat → Nat) : Prop := ∀ i < n, g i < n

def one_one_below (n : Nat) (g : Nat → Nat) : Prop :=
  ∀ i1 < n, ∀ i2 < n, g i1 = g i2 → i1 = i2

def onto_below (n : Nat) (g : Nat → Nat) : Prop :=
  ∀ k < n, ∃ i < n, g i = k

def perm_below (n : Nat) (g : Nat → Nat) : Prop :=
  maps_below n g ∧ one_one_below n g ∧ onto_below n g
```

The proofs of our next two lemmas are somewhat long.  We state them now, but put off discussion of their proofs until the end of the section.  The first lemma says that, if `m` and `a` are relatively prime, then `G m a` permutes the natural numbers less than `m`, and the second says that permuting the terms of a product does not change the value of the product.

```lean
lemma G_perm_below {m a : Nat} [NeZero m]
    (h1 : rel_prime m a) : perm_below m (G m a)

lemma perm_prod {m : Nat} (f : Nat → ZMod m) :
    ∀ (n : Nat), ∀ (g : Nat → Nat), perm_below n g →
      prod_seq n 0 f = prod_seq n 0 (f ∘ g)
```

There is just one more fact we need before we can prove `Theorem_7_4_2`: all of the factors in the `F`-product are invertible, and therefore the `F`-product is invertible:

```lean
lemma F_invertible (m i : Nat) : invertible (F m i) := by
  by_cases h : rel_prime m i
  · -- Case 1. h : rel_prime m i
    rewrite [F_rp_def h]
    show invertible [i]_m from (Theorem_7_3_7 m i).rtl h
    done
  · -- Case 2. h : ¬rel_prime m i
    rewrite [F_not_rp_def h]
    apply Exists.intro [1]_m
    show [1]_m * [1]_m = [1]_m from Theorem_7_3_6_7 [1]_m
    done
  done

lemma Fprod_invertible (m : Nat) :
    ∀ (k : Nat), invertible (prod_seq k 0 (F m)) := by
  by_induc
  · -- Base Case
    apply Exists.intro [1]_m
    show prod_seq 0 0 (F m) * [1]_m = [1]_m from
      calc prod_seq 0 0 (F m) * [1]_m
        _ = [1]_m * [1]_m := by rw [prod_seq_base]
        _ = [1]_m := Theorem_7_3_6_7 ([1]_m)
    done
  · -- Induction Step
    fix k : Nat
    assume ih : invertible (prod_seq k 0 (F m))
    rewrite [prod_seq_zero_step]
    show invertible (prod_seq k 0 (F m) * (F m k)) from
      (prod_inv_iff_inv ih (F m k)).rtl (F_invertible m k)
    done
  done
```

We now have everything we need to prove `Theorem_7_4_2`:

```lean
theorem Theorem_7_4_2 {m a : Nat} [NeZero m] (h1 : rel_prime m a) :
    [a]_m ^ (phi m) = [1]_m := by
  have h2 : invertible (prod_seq m 0 (F m)) := Fprod_invertible m m
  obtain (Y : ZMod m) (h3 : prod_seq m 0 (F m) * Y = [1]_m) from h2
  show [a]_m ^ (phi m) = [1]_m from
    calc [a]_m ^ (phi m)
      _ = [a]_m ^ (phi m) * [1]_m := (Theorem_7_3_6_7 _).symm
      _ = [a]_m ^ (phi m) * (prod_seq m 0 (F m) * Y) := by rw [h3]
      _ = ([a]_m ^ (phi m) * prod_seq m 0 (F m)) * Y := by ring
      _ = prod_seq m 0 (F m ∘ G m a) * Y := by rw [FG_prod h1 m, phi_def]
      _ = prod_seq m 0 (F m) * Y := by
            rw [perm_prod (F m) m (G m a) (G_perm_below h1)]
      _ = [1]_m := by rw [h3]
  done
```

Rephrasing this theorem in terms of numbers gives us the usual statement of Euler's theorem:

```lean
lemma Exercise_7_4_5_Int (m : Nat) (a : Int) :
    ∀ (n : Nat), [a]_m ^ n = [a ^ n]_m := sorry

lemma Exercise_7_4_5_Nat (m a n : Nat) :
    [a]_m ^ n = [a ^ n]_m := by
  rewrite [Exercise_7_4_5_Int]
  rfl
  done

theorem Euler's_theorem {m a : Nat} [NeZero m]
    (h1 : rel_prime m a) : a ^ (phi m) ≡ 1 (MOD m) := by
  have h2 : [a]_m ^ (phi m) = [1]_m := Theorem_7_4_2 h1
  rewrite [Exercise_7_4_5_Nat m a (phi m)] at h2
    --h2 : [a ^ phi m]_m = [1]_m
  show a ^ (phi m) ≡ 1 (MOD m) from (cc_eq_iff_congr _ _ _).ltr h2
  done

#eval gcd 10 7     --Answer: 1.  So 10 and 7 are relatively prime

#eval 7 ^ phi 10   --Answer: 2401, which is congruent to 1 mod 10.
```

We now turn to the two lemmas whose proofs we skipped over, `G_perm_below` and `perm_prod`.  To prove `G_perm_below`, we must prove three facts: `maps_below m (G m a)`, `one_one_below m (G m a)`, and `onto_below m (G m a)`.  The first is straightforward:

```lean
lemma G_maps_below (m a : Nat) [NeZero m] : maps_below m (G m a) := by
  define             --Goal : ∀ i < m, G m a i < m
  fix i : Nat
  assume h1 : i < m
  rewrite [G_def]    --Goal : a * i % m < m
  show a * i % m < m from mod_nonzero_lt (a * i) (NeZero.ne m)
  done
```

For the second and third, we start with lemmas that are reminiscent of Theorem 5.3.3.

```lean
lemma right_inv_onto_below {n : Nat} {g g' : Nat → Nat}
    (h1 : ∀ i < n, g (g' i) = i) (h2 : maps_below n g') :
    onto_below n g := by
  define at h2; define
  fix k : Nat
  assume h3 : k < n
  apply Exists.intro (g' k)
  show g' k < n ∧ g (g' k) = k from And.intro (h2 k h3) (h1 k h3)
  done

lemma left_inv_one_one_below {n : Nat} {g g' : Nat → Nat}
    (h1 : ∀ i < n, g' (g i) = i) : one_one_below n g := sorry
```

To apply these lemmas with `g = G m a`, we need a function to play the role of `g'`.  A natural choice is `G m a'`, where `a'` is chosen so that `[a']_m` is the multiplicative inverse of `[a]_m`.  We know from earlier work that if `m` and `a` are relatively prime then the multiplicative inverse of `[a]_m` is `[gcd_c2 m a]_m`.  However, in the notation `G m a'`, we can't let `a' = gcd_c2 m a`, because  `a'` must be a natural number and `gcd_c2 a` is an integer.  And we can't simply coerce an integer to be a natural number---what if it's negative?  But we know `[gcd_c2 m a]_m = [(gcd_c2 m a) % m]_m` and `0 ≤ (gcd_c2 m a) % m`, and there is a function, `Int.toNat`, that will convert a nonnegative integer to a natural number.  So we make the following definitions:

```lean
def inv_mod (m a : Nat) : Nat := Int.toNat ((gcd_c2 m a) % m)

def Ginv (m a i : Nat) : Nat := G m (inv_mod m a) i
```

Now `Ginv m a` can play the role of `g'` in the last two lemmas.  We'll skip the details and just summarize the results.

```lean
lemma Ginv_right_inv {m a : Nat} [NeZero m] (h1 : rel_prime m a) :
    ∀ i < m, G m a (Ginv m a i) = i := sorry

lemma Ginv_left_inv {m a : Nat} [NeZero m] (h1 : rel_prime m a) :
    ∀ i < m, Ginv m a (G m a i) = i := sorry

lemma Ginv_maps_below (m a : Nat) [NeZero m] :
    maps_below m (Ginv m a) := G_maps_below m (inv_mod m a)

lemma G_one_one_below {m a : Nat} [NeZero m] (h1 : rel_prime m a) :
    one_one_below m (G m a) :=
  left_inv_one_one_below (Ginv_left_inv h1)

lemma G_onto_below {m a : Nat} [NeZero m] (h1 : rel_prime m a) :
    onto_below m (G m a) :=
  right_inv_onto_below (Ginv_right_inv h1) (Ginv_maps_below m a)

lemma G_perm_below {m a : Nat} [NeZero m] (h1 : rel_prime m a) :
    perm_below m (G m a) := And.intro (G_maps_below m a)
  (And.intro (G_one_one_below h1) (G_onto_below h1))
```

Finally, we turn to the proof of `perm_prod`.  Our proof will be by mathematical induction.  In the induction step, our induction hypothesis will be

::: {.ind}
```
∀ (g : Nat → Nat), perm_below n g →
    prod_seq n 0 f = prod_seq n 0 (f ∘ g),
```
:::

and we will have to prove

::: {.ind}
```
∀ (g : Nat → Nat), perm_below (n + 1) g →
    prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g).
```
:::

To prove this, we'll introduce an arbitrary function `g : Nat → Nat` and assume `perm_below (n + 1) g`.  How can we make use of the inductive hypothesis?  Here's the key idea:  Since `g` permutes the numbers below `n + 1`, there must be some `u ≤ n` such that `g u = n`.  Now let `s` be a function that swaps `u` and `n`, but leaves all other numbers fixed.  In other words, `s u = n`, `s n = u`, and `s i = i` if `i ≠ u` and `i ≠ n`.  It is not hard to show that `s` permutes the numbers below `n + 1`, and using that fact we can prove that `g ∘ s` permutes the numbers below `n + 1`.  But notice that

::: {.ind}
```
(g ∘ s) n = g (s n) = g u = n.
```
:::

In other words, `g ∘ s` leaves `n` fixed.  Using that fact, we'll be able to prove that `g ∘ s` permutes the numbers below `n`.  We can therefore apply the inductive hypothesis to `g ∘ s`, which leads to the conclusion

::: {.ind}
```
prod_seq n 0 f = prod_seq n 0 (f ∘ g ∘ s).
```
:::

Since we also have `(f ∘ g ∘ s) n = f ((g ∘ s) n) = f n`, we can extend this to

::: {.ind}
```
prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g ∘ s).
```
:::

Finally, we can then reach the required conclusion by proving

::: {.ind}
```
prod_seq (n + 1) 0 (f ∘ g ∘ s) = prod_seq (n + 1) 0 (f ∘ g).
```
:::

To carry out this plan, we begin by defining our "swapping" function and proving its properties.

```lean
def swap (u v i : Nat) : Nat :=
  if i = u then v else if i = v then u else i

lemma swap_fst (u v : Nat) : swap u v u = v := by
  define : swap u v u
    --Goal : (if u = u then v else if u = v then u else u) = v
  have h : u = u := by rfl
  rewrite [if_pos h]
  rfl
  done

lemma swap_snd (u v : Nat) : swap u v v = u := sorry

lemma swap_perm_below {u v n} (h1 : u < n) (h2 : v < n) :
    perm_below n (swap u v) := sorry
```

For the swapping function `s` in the proof outline above, we'll use `swap u n`.  To prove that `g ∘ swap u n` permutes the numbers below `n`, we'll need two lemmas:

```lean
lemma comp_perm_below {n : Nat} {f g : Nat → Nat}
    (h1 : perm_below n f) (h2 : perm_below n g) :
    perm_below n (f ∘ g) := sorry

lemma perm_below_fixed {n : Nat} {g : Nat → Nat}
    (h1 : perm_below (n + 1) g) (h2 : g n = n) : perm_below n g := sorry
```

For the final step of the proof, we'll need several lemmas

```lean
lemma break_prod_twice  {m u j n : Nat} (f : Nat → ZMod m)
    (h1 : n = u + 1 + j) : prod_seq (n + 1) 0 f =
      prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n := sorry

lemma swap_prod_eq_prod_below {m u n : Nat} (f : Nat → ZMod m)
    (h1 : u ≤ n) : prod_seq u 0 (f ∘ swap u n) = prod_seq u 0 f := sorry

lemma swap_prod_eq_prod_between {m u j n : Nat} (f : Nat → ZMod m)
    (h1 : n = u + 1 + j) : prod_seq j (u + 1) (f ∘ swap u n) =
      prod_seq j (u + 1) f := sorry

lemma trivial_swap (u : Nat) : swap u u = id := sorry
```

Using these lemmas, we can prove the fact we'll need in the final step.

```lean
lemma swap_prod_eq_prod {m u n : Nat} (f : Nat → ZMod m) (h1 : u ≤ n) :
    prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f := by
  by_cases h2 : u = n
  · -- Case 1. h2 : u = n
    rewrite [h2, trivial_swap n]
      --Goal : prod_seq (n + 1) 0 (f ∘ id) = prod_seq (n + 1) 0 f
    rfl
    done
  · -- Case 2. h2 : ¬u = n
    have h3 : u + 1 ≤ n := Nat.lt_of_le_of_ne h1 h2
    obtain (j : Nat) (h4 : n = u + 1 + j) from Nat.exists_eq_add_of_le h3
    have break_f : prod_seq (n + 1) 0 f =
      prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n :=
      break_prod_twice f h4
    have break_fs : prod_seq (n + 1) 0 (f ∘ swap u n) =
      prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u *
      prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n :=
      break_prod_twice (f ∘ swap u n) h4
    have f_eq_fs_below : prod_seq u 0 (f ∘ swap u n) =
      prod_seq u 0 f := swap_prod_eq_prod_below f h1
    have f_eq_fs_btwn : prod_seq j (u + 1) (f ∘ swap u n) =
      prod_seq j (u + 1) f := swap_prod_eq_prod_between f h4
    show prod_seq (n + 1) 0 (f ∘ swap u n) = prod_seq (n + 1) 0 f from
      calc prod_seq (n + 1) 0 (f ∘ swap u n)
        _ = prod_seq u 0 (f ∘ swap u n) * (f ∘ swap u n) u *
            prod_seq j (u + 1) (f ∘ swap u n) * (f ∘ swap u n) n :=
              break_fs
        _ = prod_seq u 0 f * (f ∘ swap u n) u *
            prod_seq j (u + 1) f * (f ∘ swap u n) n := by
              rw [f_eq_fs_below, f_eq_fs_btwn]
        _ = prod_seq u 0 f * f (swap u n u) *
            prod_seq j (u + 1) f * f (swap u n n) := by rfl
        _ = prod_seq u 0 f * f n * prod_seq j (u + 1) f * f u := by
              rw [swap_fst, swap_snd]
        _ = prod_seq u 0 f * f u * prod_seq j (u + 1) f * f n := by ring
        _ = prod_seq (n + 1) 0 f := break_f.symm
    done
  done
```

We finally have all the pieces in place to prove `perm_prod`:

```lean
lemma perm_prod {m : Nat} (f : Nat → ZMod m) :
    ∀ (n : Nat), ∀ (g : Nat → Nat), perm_below n g →
      prod_seq n 0 f = prod_seq n 0 (f ∘ g) := by
  by_induc
  · -- Base Case
    fix g : Nat → Nat
    assume h1 : perm_below 0 g
    rewrite [prod_seq_base, prod_seq_base]
    rfl
    done
  · -- Induction Step
    fix n : Nat
    assume ih : ∀ (g : Nat → Nat), perm_below n g →
      prod_seq n 0 f = prod_seq n 0 (f ∘ g)
    fix g : Nat → Nat
    assume g_pb : perm_below (n + 1) g
    define at g_pb
    have g_ob : onto_below (n + 1) g := g_pb.right.right
    define at g_ob
    have h1 : n < n + 1 := by linarith
    obtain (u : Nat) (h2 : u < n + 1 ∧ g u = n) from g_ob n h1
    have s_pb : perm_below (n + 1) (swap u n) :=
      swap_perm_below h2.left h1
    have gs_pb_n1 : perm_below (n + 1) (g ∘ swap u n) :=
      comp_perm_below g_pb s_pb
    have gs_fix_n : (g ∘ swap u n) n = n :=
      calc (g ∘ swap u n) n
        _ = g (swap u n n) := by rfl
        _ = g u := by rw [swap_snd]
        _ = n := h2.right
    have gs_pb_n : perm_below n (g ∘ swap u n) :=
      perm_below_fixed gs_pb_n1 gs_fix_n
    have gs_prod : prod_seq n 0 f = prod_seq n 0 (f ∘ (g ∘ swap u n)) :=
      ih (g ∘ swap u n) gs_pb_n
    have h3 : u ≤ n := by linarith
    show prod_seq (n + 1) 0 f = prod_seq (n + 1) 0 (f ∘ g) from
      calc prod_seq (n + 1) 0 f
        _ = prod_seq n 0 f * f n := prod_seq_zero_step n f
        _ = prod_seq n 0 (f ∘ (g ∘ swap u n)) *
            f ((g ∘ swap u n) n) := by rw [gs_prod, gs_fix_n]
        _ = prod_seq n 0 (f ∘ g ∘ swap u n) *
            (f ∘ g ∘ swap u n) n := by rfl
        _ = prod_seq (n + 1) 0 (f ∘ g ∘ swap u n) :=
              (prod_seq_zero_step n (f ∘ g ∘ swap u n)).symm
        _ = prod_seq (n + 1) 0 ((f ∘ g) ∘ swap u n) := by rfl
        _ = prod_seq (n + 1) 0 (f ∘ g) := swap_prod_eq_prod (f ∘ g) h3
    done
  done
```

There is one more theorem that is proven in Section 7.4 of *HTPI*: Theorem 7.4.4, which says that $\varphi$ is a multiplicative function.  The proof requires ideas that we will not develop in Lean until Chapter 8, so we will put off the proof until Section 8.1½.

### Exercises

::: {.numex arguments="1"}
```lean
--Hint:  Use induction.
--For the base case, compute [a]_m ^ 0 * [1]_m in two ways:
--by Theorem_7_3_6_7, [a] ^ 0 * [1]_m = [a]_m ^ 0
--by ring, [a]_m ^ 0 * [1]_m = [1]_m.
lemma Exercise_7_4_5_Int (m : Nat) (a : Int) :
    ∀ (n : Nat), [a]_m ^ n = [a ^ n]_m := sorry
```
:::

::: {.numex arguments="2"}
```lean
lemma left_inv_one_one_below {n : Nat} {g g' : Nat → Nat}
    (h1 : ∀ i < n, g' (g i) = i) : one_one_below n g := sorry
```
:::

::: {.numex arguments="3"}
```lean
lemma comp_perm_below {n : Nat} {f g : Nat → Nat}
    (h1 : perm_below n f) (h2 : perm_below n g) :
    perm_below n (f ∘ g) := sorry
```
:::

::: {.numex arguments="4"}
```lean
lemma perm_below_fixed {n : Nat} {g : Nat → Nat}
    (h1 : perm_below (n + 1) g) (h2 : g n = n) : perm_below n g := sorry
```
:::

::: {.numex arguments="5"}
```lean
lemma Lemma_7_4_6 {a b c : Nat} :
    rel_prime (a * b) c ↔ rel_prime a c ∧ rel_prime b c := sorry
```
:::

::: {.numex arguments="6"}
```lean
example {m a : Nat} [NeZero m] (h1 : rel_prime m a) :
    a ^ (phi m + 1) ≡ a (MOD m) := sorry
```
:::

::: {.numex arguments="7"}
```lean
theorem Like_Exercise_7_4_11 {m a p : Nat} [NeZero m]
    (h1 : rel_prime m a) (h2 : p + 1 = phi m) :
    [a]_m * [a ^ p]_m = [1]_m := sorry
```
:::

::: {.numex arguments="8"}
```lean
theorem Like_Exercise_7_4_12 {m a p q k : Nat} [NeZero m]
    (h1 : rel_prime m a) (h2 : p = q + (phi m) * k) :
    a ^ p ≡ a ^ q (MOD m) := sorry
```
:::

## 7.5. Public-Key Cryptography

Section 7.5 of *HTPI* discusses the RSA public-key cryptography system.  The system is based on the following theorem:

```lean
theorem Theorem_7_5_1 (p q n e d k m c : Nat)
    (p_prime : prime p) (q_prime : prime q) (p_ne_q : p ≠ q)
    (n_pq : n = p * q) (ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1)
    (h1 : [m]_n ^ e = [c]_n) : [c]_n ^ d = [m]_n
```

For an explanation of how the RSA system works and why `Theorem_7_5_1` justifies it, see *HTPI*.  Here we will focus on proving the theorem in Lean.

We will be applying Euler's theorem to the prime numbers `p` and `q`, so we will need to know how to compute `phi p` and `phi q`.  Fortunately, there is a simple formula we can use.

```lean
lemma num_rp_prime {p : Nat} (h1 : prime p) :
    ∀ k < p, num_rp_below p (k + 1) = k := sorry

lemma phi_prime {p : Nat} (h1 : prime p) : phi p = p - 1 := by
  have h2 : 1 ≤ p := prime_pos h1
  have h3 : p - 1 + 1 = p := Nat.sub_add_cancel h2
  have h4 : p - 1 < p := by linarith
  have h5 : num_rp_below p (p - 1 + 1) = p - 1 :=
    num_rp_prime h1 (p - 1) h4
  rewrite [h3] at h5
  show phi p = p - 1 from h5
  done
```

We will also need to use Lemma 7.4.5 from *HTPI*.  To prove that lemma in Lean, we will use `Theorem_7_2_2`, which says that for natural numbers `a`, `b`, and `c`, if `c ∣ a * b` and `c` and `a` are relatively prime, then `c ∣ b`.  But we will need to extend the theorem to allow `b` to be an integer rather than a natural number.  To prove this extension, we use the Lean function `Int.natAbs : Int → Nat`, which computes the absolute value of an integer.  Lean knows several theorems about this function:

::: {.ind}
```
@Int.natCast_dvd : ∀ {n : ℤ} {m : ℕ}, ↑m ∣ n ↔ m ∣ Int.natAbs n

Int.natAbs_mul : ∀ (a b : ℤ),
                  Int.natAbs (a * b) = Int.natAbs a * Int.natAbs b

Int.natAbs_ofNat : ∀ (n : ℕ), Int.natAbs ↑n = n
```
:::

With the help of these theorems, our extended version of `Theorem_7_2_2` follows easily from the original version:

```lean
theorem Theorem_7_2_2_Int {a c : Nat} {b : Int}
    (h1 : ↑c ∣ ↑a * b) (h2 : rel_prime a c) : ↑c ∣ b := by
  rewrite [Int.natCast_dvd, Int.natAbs_mul,
    Int.natAbs_ofNat] at h1        --h1 : c ∣ a * Int.natAbs b
  rewrite [Int.natCast_dvd]        --Goal : c ∣ Int.natAbs b
  show c ∣ Int.natAbs b from Theorem_7_2_2 h1 h2
  done
```

With that preparation, we can now prove `Lemma_7_4_5`.

```lean
lemma Lemma_7_4_5 {m n : Nat} (a b : Int) (h1 : rel_prime m n) :
    a ≡ b (MOD m * n) ↔ a ≡ b (MOD m) ∧ a ≡ b (MOD n) := by
  apply Iff.intro
  · -- (→)
    assume h2 : a ≡ b (MOD m * n)
    obtain (j : Int) (h3 : a - b = (m * n) * j) from h2
    apply And.intro
    · -- Proof of a ≡ b (MOD m)
      apply Exists.intro (n * j)
      show a - b = m * (n * j) from
        calc a - b
          _ = m * n * j := h3
          _ = m * (n * j) := by ring
      done
    · -- Proof of a ≡ b (MOD n)
      apply Exists.intro (m * j)
      show a - b = n * (m * j) from
        calc a - b
          _ = m * n * j := h3
          _ = n * (m * j) := by ring
      done
    done
  · -- (←)
    assume h2 : a ≡ b (MOD m) ∧ a ≡ b (MOD n)
    obtain (j : Int) (h3 : a - b = m * j) from h2.left
    have h4 : (↑n : Int) ∣ a - b := h2.right
    rewrite [h3] at h4      --h4 : ↑n ∣ ↑m * j
    have h5 : ↑n ∣ j := Theorem_7_2_2_Int h4 h1
    obtain (k : Int) (h6 : j = n * k) from h5
    apply Exists.intro k    --Goal : a - b = ↑(m * n) * k
    rewrite [Nat.cast_mul]  --Goal : a - b = ↑m * ↑n * k
    show a - b = (m * n) * k from
      calc a - b
        _ = m * j := h3
        _ = m * (n * k) := by rw [h6]
        _ = (m * n) * k := by ring
    done
  done
```

Finally, we will need an exercise from Section 7.2, and we will need to know `NeZero p` for prime numbers `p`:

```lean
theorem rel_prime_symm {a b : Nat} (h : rel_prime a b) :
    rel_prime b a := sorry

lemma prime_NeZero {p : Nat} (h : prime p) : NeZero p := by
  rewrite [neZero_iff]     --Goal : p ≠ 0
  define at h
  linarith
  done
```

Much of the reasoning about modular arithmetic that we need for the proof of `Theorem_7_5_1` is contained in a technical lemma:

```lean
lemma Lemma_7_5_1 {p e d m c s : Nat} {t : Int}
    (h1 : prime p) (h2 : e * d = (p - 1) * s + 1)
    (h3 : m ^ e - c = p * t) :
    c ^ d ≡ m (MOD p) := by
  have h4 : m ^ e ≡ c (MOD p) := Exists.intro t h3
  have h5 : [m ^ e]_p = [c]_p := (cc_eq_iff_congr _ _ _).rtl h4
  rewrite [←Exercise_7_4_5_Nat] at h5  --h5 : [m]_p ^ e = [c]_p
  by_cases h6 : p ∣ m
  · -- Case 1. h6 : p ∣ m
    have h7 : m ≡ 0 (MOD p) := by
      obtain (j : Nat) (h8 : m = p * j) from h6
      apply Exists.intro (↑j : Int)   --Goal : ↑m - 0 = ↑p * ↑j
      rewrite [h8, Nat.cast_mul]
      ring
      done
    have h8 : [m]_p = [0]_p := (cc_eq_iff_congr _ _ _).rtl h7
    have h9 : e * d ≠ 0 := by
      rewrite [h2]
      show (p - 1) * s + 1 ≠ 0 from Nat.add_one_ne_zero _
      done
    have h10 : (0 : Int) ^ (e * d) = 0 := zero_pow h9
    have h11 : [c ^ d]_p = [m]_p :=
      calc [c ^ d]_p
        _ = [c]_p ^ d := by rw [Exercise_7_4_5_Nat]
        _ = ([m]_p ^ e) ^ d := by rw [h5]
        _ = [m]_p ^ (e * d) := by ring
        _ = [0]_p ^ (e * d) := by rw [h8]
        _ = [0 ^ (e * d)]_p := Exercise_7_4_5_Int _ _ _
        _ = [0]_p := by rw [h10]
        _ = [m]_p := by rw [h8]
    show c ^ d ≡ m (MOD p) from (cc_eq_iff_congr _ _ _).ltr h11
    done
  · -- Case 2. h6 : ¬p ∣ m
    have h7 : rel_prime m p := rel_prime_of_prime_not_dvd h1 h6
    have h8 : rel_prime p m := rel_prime_symm h7
    have h9 : NeZero p := prime_NeZero h1
    have h10 : (1 : Int) ^ s = 1 := by ring
    have h11 : [c ^ d]_p = [m]_p :=
      calc [c ^ d]_p
        _ = [c]_p ^ d := by rw [Exercise_7_4_5_Nat]
        _ = ([m]_p ^ e) ^ d := by rw [h5]
        _ = [m]_p ^ (e * d) := by ring
        _ = [m]_p ^ ((p - 1) * s + 1) := by rw [h2]
        _ = ([m]_p ^ (p - 1)) ^ s * [m]_p := by ring
        _ = ([m]_p ^ (phi p)) ^ s * [m]_p := by rw [phi_prime h1]
        _ = [1]_p ^ s * [m]_p := by rw [Theorem_7_4_2 h8]
        _ = [1 ^ s]_p * [m]_p := by rw [Exercise_7_4_5_Int]
        _ = [1]_p * [m]_p := by rw [h10]
        _ = [m]_p * [1]_p := by ring
        _ = [m]_p := Theorem_7_3_6_7 _
    show c ^ d ≡ m (MOD p) from (cc_eq_iff_congr _ _ _).ltr h11
    done
  done
```

Here, finally, is the proof of `Theorem_7_5_1`:

```lean
theorem Theorem_7_5_1 (p q n e d k m c : Nat)
    (p_prime : prime p) (q_prime : prime q) (p_ne_q : p ≠ q)
    (n_pq : n = p * q) (ed_congr_1 : e * d = k * (p - 1) * (q - 1) + 1)
    (h1 : [m]_n ^ e = [c]_n) : [c]_n ^ d = [m]_n := by
  rewrite [Exercise_7_4_5_Nat, cc_eq_iff_congr] at h1
    --h1 : m ^ e ≡ c (MOD n)
  rewrite [Exercise_7_4_5_Nat, cc_eq_iff_congr]
    --Goal : c ^ d ≡ m (MOD n)
  obtain (j : Int) (h2 : m ^ e - c = n * j) from h1
  rewrite [n_pq, Nat.cast_mul] at h2
    --h2 : m ^ e - c = p * q * j
  have h3 : e * d = (p - 1) * (k * (q - 1)) + 1 := by
    rewrite [ed_congr_1]
    ring
    done
  have h4 : m ^ e - c = p * (q * j) := by
    rewrite [h2]
    ring
    done
  have congr_p : c ^ d ≡ m (MOD p) := Lemma_7_5_1 p_prime h3 h4
  have h5 : e * d = (q - 1) * (k * (p - 1)) + 1 := by
    rewrite [ed_congr_1]
    ring
    done
  have h6 : m ^ e - c = q * (p * j) := by
    rewrite [h2]
    ring
    done
  have congr_q : c ^ d ≡ m (MOD q) := Lemma_7_5_1 q_prime h5 h6
  have h7 : ¬q ∣ p := by
    by_contra h8
    have h9 : q = 1 ∨ q = p := dvd_prime p_prime h8
    disj_syll h9 (prime_not_one q_prime)
    show False from p_ne_q h9.symm
    done
  have h8 : rel_prime p q := rel_prime_of_prime_not_dvd q_prime h7
  rewrite [n_pq, Lemma_7_4_5 _ _ h8]
  show c ^ d ≡ m (MOD p) ∧ c ^ d ≡ m (MOD q) from
    And.intro congr_p congr_q
  done
```

### Exercises

::: {.numex arguments="1"}
```lean
--Hint:  Use induction.
lemma num_rp_prime {p : Nat} (h1 : prime p) :
    ∀ k < p, num_rp_below p (k + 1) = k := sorry
```
:::

::: {.numex arguments="2"}
```lean
lemma three_prime : prime 3 := sorry
```
:::

::: {.numex arguments="3"}
```lean
--Hint:  Use the previous exercise, Exercise_7_2_7, and Theorem_7_4_2.
theorem Exercise_7_5_13a (a : Nat) (h1 : rel_prime 561 a) :
    a ^ 560 ≡ 1 (MOD 3) := sorry
```
:::

::: {.numex arguments="4"}
```lean
--Hint:  Imitate the way Theorem_7_2_2_Int was proven from Theorem_7_2_2.
lemma Theorem_7_2_3_Int {p : Nat} {a b : Int}
    (h1 : prime p) (h2 : ↑p ∣ a * b) : ↑p ∣ a ∨ ↑p ∣ b := sorry
```
:::

::: {.numex arguments="5"}
```lean
--Hint:  Use the previous exercise.
theorem Exercise_7_5_14b (n : Nat) (b : Int)
    (h1 : prime n) (h2 : b ^ 2 ≡ 1 (MOD n)) :
    b ≡ 1 (MOD n) ∨ b ≡ -1 (MOD n) := sorry
```
:::