Exercise 8.1
In Section 8.7, we gave the name $p(m,n,u)$ to a proof of the proposition
$$∃x,y : \mathbb{Z}. (mx+ny = 1)$$
in the context $Γ ≡ m : \mathbb{N}^+, n : \mathbb{N}^+, u : coprime(m,n)$.
Assume that we have constructed, in context $m : \mathbb{N}^+, n : \mathbb{N}^+$, a proof (i.e. an inhabitant) $q(m,n)$ of the proposition
$$coprime(m,n) ⇒coprime(n,m)$$
Find an inhabitant of
$$∃x,y : \mathbb{Z}. (nx+my = 1)$$
in context $Γ$.
We start with $p$ which is the name given to the proof of the proposition
$$ \exists x,y : \mathbb{Z}. (mx+ny = 1) \tag{i}$$
The name also carries with it the ordered list of arguments $(m,n,u)$. The first two arguments are the positive natural numbers $n$ and $m$ expected by the proof. The third argument is a proof that the first two arguments, $m$ and $n$ (in that order), are co-prime.
We want to prove the proposition
$$ \exists x,y : \mathbb{Z}. (nx+my = 1) \tag{ii}$$
The order of $n$ and $m$ is different to (i), and this means $p(m,n,u)$ is not a proof of (ii).
We are given a proof $q(m,n)$ of the proposition $coprime(m,n) \implies coprime(n,m)$, that is
$$q(m,n) \; : \; coprime(m,n) \implies coprime(n,m)$$
So the proof $q(m,n)$ applied to $u$, the proof $coprime(m,n)$, gives us a proof $coprime(n,m)$.
$$ q(m,n)u \; : \; coprime(n,m)$$
We also check that the context of $q$ allows it to be used in the context in which we apply it to $u$, that is, $\Gamma$. The context of $q$ us a subset of $\Gamma$ so can be used, and it can be used with $u$ because $u$ is defined in $\Gamma$.
If we are to use $p$ as a proof of $∃x,y : \mathbb{Z}. (nx+my = 1)$, the order of the variables $n$ and $m$ require the proof to be of the form $p(n,m,?)$ and not $p(m,n,?)$. The $?$ a proof that $n$ and $m$ (in that order) are co-prime. We have that from above.
And so $p(n,m,q(m,n)u)$ is a proof of the proposition (ii). That is
$$ \Gamma \; \triangleright \; p(n,m,q(m,n)u) \; : \; \exists x,y:\mathbb{Z}.(nx + my = 1)$$
We can choose to give this proof a name, $r(m,n.u)$
$$ \Gamma \; \triangleright \; r(m,n,u) \; := \; p(n,m,q(m,n)u) \; : \; \exists x,y:\mathbb{Z}.(nx + my = 1)$$
