In the following, we work with vectors and matrices whose entries are rational numbers. Inequalities between such vectors are understood to be coordinatewise: e.g., two vectors $a = \left(a_1,a_2,\ldots,a_n\right)^T$ and $b = \left(b_1,b_2,\ldots,b_n\right)^T$ are said to satisfy $a > b$ if and only if each $i \in \left\{1,2,\ldots,n\right\}$ satisfies $a_i > b_i$.

Theorem 1. Let $n$ be a positive integer. Let $A$ be an $n\times n$-matrix whose entries are nonnegative rational numbers. Then, there exists a nonzero vector $v \in \mathbb{Q}^n$ with nonnegative coordinates such that either $Av \geq v$ or $Av < v$.

The next theorem concerns a more restricted class of matrices. If $A$ is an $n\times n$-matrix whose entries are nonnegative rational numbers, then we define $D_A$ to be the directed graph whose vertices are the numbers $1,2,\ldots,n$, and which has an arc from vertex $i$ to vertex $j$ if and only if the $\left(i,j\right)$-th entry of $A$ is positive. We say that the matrix $A$ is irreducible if and only if this digraph $D_A$ is strongly connected. (Other equivalent definitions of irreducibility appear on the Wikipedia page for Perron-Frobenius.)

Theorem 2. Let $n$ be a positive integer. Let $A$ be an irreducible $n\times n$-matrix whose entries are nonnegative rational numbers. Then, there exists a nonzero vector $v \in \mathbb{Q}^n$ with positive coordinates such that either $Av > v$ or $Av = v$ or $Av < v$.

These two theorems can both be derived (with some nontrivial but not too hard work) from the Perron-Frobenius theorem. The latter constructs a Perron-Frobenius eigenvector of $A$ with real coordinates; one just needs to approximate its coordinates by rational numbers (unless it has eigenvalue $1$, in which case we have to make sure the approximation happens in the $1$-eigenspace).

Question. How can Theorem 1 and Theorem 2 be proven in constructive logic?

(Roughly speaking, this is probably tantamount to not using real numbers in the proof -- or building up the theory of real algebraics in constructive logic, which seems to have been done but I haven't seen it properly written up, and even then I don't know if Perron-Frobenius still applies and how you would prove it. Simon Henry's approximate version of Brouwer's fixed point theorem might help, but I don't know how it is proven.)

I'm asking partly because of recent uses of Theorems 1 and 2 in combinatorics, but this question has been in the back of my mind for many years, ever after I solved a restricted version of the $n = 3$ case (IMO Shortlist 2003 problem A1) (official solution) on an exam.