Strict WQOs and Strict WPOs The Wikipedia article on WQOs does not mention a strict version. I came across a particular relation, which I could only describe as a strict WQO, but I am wondering if my reasoning is correct and if the notion of a "strict WQO" even makes sense (I think it does).
Consider the set $X \times \mathbb{N}$ where $X = \{1,\ldots,k\}$ for some integer $k$ and $\mathbb{N}$ denotes the set of natural numbers. We define the relation $\prec$ as:
$$ (x_1,n_1) \prec (x_2,n_2) \quad \text{iff} \quad (x_1 \leq x_2) \wedge (n_1 < n_2) $$
Strict Quasi Order: Clearly $\prec$ is irreflexive and transitive, and therefore a strict quasi order.
No Infinite Antichains: It's also easy to observe that there are no infinite antichains. Due to the Pigeonhole principle, any sequence $(x_1,n_1), (x_2,n_2), \ldots$ of length $\geq k$ must have at least one pair $\langle (x_i,n_i),(x_j,n_j)\rangle$ such that $x_i = x_j$. Then, since either $n_i < n_j$ or $n_j < n_i$ must hold, we have at least one pair in the sequence on which $\prec$ holds.
Well-Foundedness: Finally, we show that there are no infinite descending chains. For any element $(i,j)$, there are only $|\{1,\ldots,i\} \times \{1,\ldots,(j-1)\}| = i(j-1)$ elements that can precede $(i,j)$.
Is this reasoning correct? Then is $\prec$ a strict WQO on $X \times \mathbb{N}$?
Related questions:
Since antisymmetry is implied by irreflexivity and transitivity, is any strict quasi order also a strict partial order? And so is any strict WQO also a strict WPO?
Thanks.
 A: If $\leq$ is any relation, let $<$ be the strict version when $x<y$ if and only if ($x\leq y$ and $x\neq y$). There's really not much more to defining a strict relation. Note that we can alternatively start with $<$ and define $x\leq y$ as ($x<y$ or $x=y$).
So, to check that your $\prec$ relation is a strict WQO, we define $\preceq$ as $x\preceq y$ if and only if ($x\prec y$ or $x=y$).


*

*$\preceq$ is reflexive by definition, since $x=x$ implies $x\preceq x$

*$\preceq$ is transitive: this follows easily from the transitivity of $\leq$ and $<$ on $X$ and $\mathbb N$ respectively.

*Well-founded: let $\langle (x_i,n_i)\mid i\in\mathbb N\rangle$ be an infinite sequence. By the infinite pigeonhole principle and $X$ being finite, there is an $x\in X$ such that $I=\{i\in \mathbb N\mid x_i=x\}$ is infinite. Let $\langle(x,n_i)\mid i\in I\rangle$ be the subsequence consisting of those elements, then $(x,n_i)\preceq(x,n_j)$ iff $n_i\leq n_j$. Since $\mathbb N$ is well-ordered, there must be $i,j\in I$ such that $i<j$ and $n_i\leq n_j$, hence there exist $i<j$ such that $(x_i,n_i)\preceq(x_j,n_j)$.


Now, the relation $\preceq$ is antisymmetric as well: if $(x,n)\neq(y,m)$ and $(x,n)\preceq(y,m)$, then $n<m$, thus $m\not <n$, thus $(y,m)\not\preceq(x,n)$. Therefore $\preceq$ is in fact a WPO.

It is true that antisymmetry is implied by irreflexivity and transitivity. However, it is not true that a strict WQO is transitive. 
As a very simple example, take $\{a,b\}$ with the universal relation ${\trianglelefteq}=\{(a,b),(b,a),(a,a),(b,b)\}$. It is easy to see this is a WQO and not a WPO. However, the strict relation $\triangleleft=\{(a,b),(b,a)\}$  is no longer transitive.
