I want to apply the proof strategies and overall scratch work diagram based framework introduced in the book "How to Prove It" in order to rewrite the following theorem:
Theorem Any positive rational number has an expression as a fraction in lowest form.
Proof. First write a given positive rational number as a quotient of positive integers $\frac{m}{n}$. We know that 1 is a common divisor of $m$ and $n$. Furthermore, any common divisor is at most equal to $m$ or $n$. Thus among all common divisors there is a greatest one, which we denote by $d$. Thus we can write $$ m = dr \qquad \text{and} \qquad n = ds $$ with positive integers $r$ and $s$. Our rational number is equal to $$ \frac{m}{n} = \frac{dr}{ds} = \frac{r}{s} $$
All we have to do now is to show that the only common divisor of $r$ and $s$ is $1$. Suppose that $e$ is a common divisor which is greater than 1. Then we can write $$ r = ex \qquad \text{and} \qquad s = ey $$ with positive integers $x$ and $y$. Hence $$ m = dr = dex \qquad \text{and} \qquad n = ds = dey $$ Therefore $de$ is a common divisor for $m$ and $n$, and is greater than $d$ since $e$ is greater than $1$. This is impossible because we assumed that $d$ was the greatest common divisor of $m$ and $n$. Therefore $1$ is the only common divisor of $r$ and $s$, and our theorem is proved. $\blacksquare$
The first thing that I did was to rewrite the statement using logical connectives and quantifiers $$ \forall a: (a \in \mathbb{Q}_+) \rightarrow \exists \ r,s : (r,s \in \mathbb{Z}_+) \ \land (a = r/s) \ \land (\operatorname{gcd}(r,s) = 1). $$ making it clear that we are trying to prove a conditional statement.
So we should assume that $(a \in \mathbb{Q}_+)$ and our scratch work diagram becomes \begin{array}{c c c c c} \text{Givens} & & \qquad \qquad \qquad \qquad \qquad & & \text{Goal} \\ \hline (a \in \mathbb{Q}_+) & & & & \exists \ r,s : (r,s \in \mathbb{Z}_+) \ \land (a = r/s) \ \land (\operatorname{gcd}(r,s) = 1) \\ \end{array}
How should I proceed from here? This seems like an existence proof using a proof by contradiction at some point, and while the original proof makes sense to me, I'm having trouble factoring it in small steps using this framework.