Question:
Prove constructively that if $(A_{1},\prec_{1})$ and $(A_{2},\prec_{2})$ are two well-ordered sets then their lexicographical combination $(A_{1} \times A_{2},<_{1,2})$ is also well ordered.
I have tried to spell out all the things I think are necessary to prove the desired result constructively, namely:
If $(A_{1},\prec_{1})$ and $(A_{2},\prec_{2})$ are two sets with relations, then we can form the juxtaposition of these $(A_{1} \times A_{2}, \prec_{1,2})$ \begin{equation} (a,b) \prec_{1,2} (c,d) \iff a \prec_{1} c \lor I(A_{1},a,c) \land b \prec_{2} d \end{equation} where we define \begin{align} &inl(a) \prec_{1,2} inl(b) \iff a \prec_{1} b \\ &inl(a) \prec_{1,2} inr(b) \iff \top \\ &inr(b) \prec_{1,2} inl(a) \iff \bot \\ &inr(a) \prec_{1,2} inr(b) \iff a \prec_{2} b \end{align}
Now, by definition, a well-order means that we have a well founded linear order; which is to say that for every progressive predicate $P$ on A, $(\forall x:A)P(x)$ and $x \prec_{1} y \lor x=_{1}y \lor y \prec_{1} x$.
However, I struggle to connect find a brief, sound and constructive argument that will answer the question. That is why I humble I ask this forum for help, hoping someone more enlighten may guide me to greater understanding. Thanks!